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.)
