  We consider several formalizations in the language of second-order arithmetic
of "The formula $\phi$ is a theorem of $\omega$-logic", including some which
have been studied in the literature and a new variant defined via a least fixed
point. We analyze the provability of relations between these different
formalizations in standard theories of reverse mathematics. With this, we study
the strength of various reflection principles arising from these notions of
provability, surveying known results and establishing some new equivalences,
including a characterization of $\Pi^1_1$-${\sf CA}_0$ in terms of our
fixed-point formalization of $\omega$-logic.
