# Can Gentzen-style proofs give omega-consistency and beyond?

In 1936, Gentzen famously showed that Primitive Recursive Arithmetic, plus the assumption that the ordinal $\epsilon_0$ is well-founded, is able to prove Con(PA). But of course, Con(PA) doesn't yet imply PA is sound, so we might wonder how far a Gentzen-style proof can go toward establishing soundness.

At this point, you might interject that soundness isn't even first-order definable, so of course we can't hope for a formal proof that PA is sound. But it seems to me that we can mostly sidestep that problem using Tarski's prescription, which lets us formally define soundness for whatever fixed number of quantifiers we care about (that is, for $\Sigma_k$ and $\Pi_k$ sentences for any fixed $k$). So in particular, given any fixed arithmetical sentence---let's say $P\ne NP$, which is a $\Pi_2$-sentence---it seems reasonable to hope for a proof of the following implication, within Primitive Recursive Arithmetic:

If $\epsilon_0$ is well-founded and PA proves $P\ne NP$, then $P\ne NP$ holds.

My question is, does the technology of ordinal proof theory (about which I know almost nothing) let us establish statements like the above? Also, if we want to establish such a thing for a $\Pi_k$-sentence, does the ordinal that we need increase with $k$, or does the same ordinal (e.g., $\epsilon_0$) always suffice?

(This question is a followup to my recent question about an ordinal encoding the proof strength of ZF, and arose from discussion with Timothy Chow there.)

• Yes. And what increases with $k$ is not the ordinal ($\epsilon_0$), but the complexity of the formula on which you apply transfinite induction (it will be $\Pi_{k-2}$ or something). Primitive recursive transfinite induction should suffice for $\Pi_2$-soundness. Apr 25, 2014 at 13:11
• Someone more knowledgeable with ordinal analysis should answer that, however I suspect that $\Pi_2$ is all you get. Primitive recursive TI up to $\epsilon_0$ certainly does not imply the $\Pi_4$-soundness of PA, as it is itself a $\Pi_3$-axiomatized schema. Apr 25, 2014 at 13:24
• The argument in my last comment actually applies to any computable ordinal $\alpha$. Primitive recursive TI up to $\alpha$ is still $\Pi_3$-axiomatized, and no set of true $\Pi_3$ sentences can imply the $\Sigma_3$-soundness of PA (or even of pure predicate calculus in the language of PA) due to Gödel’s theorem. Apr 25, 2014 at 13:32
• No, that’s a wrong view. We are talking about the truth of bounded complexity conclusions of full induction. Induction on $\Pi_{k+2}$ formulas has a much smaller ordinal than $\epsilon_0$, and its soundness is provable in PA itself. Apr 26, 2014 at 11:42
• Also, $\Pi_k$ transfinite induction up to $\epsilon_0$ cannot be in any useful way decomposed as plain $\Pi_k$ induction “+ $\epsilon_0$”. Apr 26, 2014 at 12:31