Impredicative consistency and reflection
David Fernández–Duque · arXiv (Cornell University) · 2015
Given a set of natural numbers, we may formalize The formula $\phi$ is a theorem of $\omega$-logic over the theory $T$ using an oracle for $X$ by an expression $[{\sf I}|X]_T \phi$, defined using a least fixed point in the language of second-order arithmetic. We will prove that the consistency and reflection principles arising from this notion of provability lead to axiomatizations of $\Pi^1_1$-$CA_0$ and $\Pi^1_1$-$CA_0$ with bar induction. We compare this to well-known results that reflection for $\omega$-derivable formulas and $\omega$-model reflection are equivalent to bar induction.