I seem to remember having read that the prooftheoretic ordinal (sup of ordinals the theory can prove wellordered) of $\mathsf{PA} + \mathsf{Con}(\mathsf{PA})$ is the same as that of $\mathsf{PA}$, namely $\epsilon_0$. However, the one particular source where I remember reading something like this is The Realm of Ordinal Analysis by Michael Rathjen (bottom of p.9), but this is less unambiguous than I thought. Is this statement true? If so, do $\mathsf{PA} + \mathsf{Con}(\mathsf{PA} + \mathsf{Con}(\mathsf{PA}))$ etc. have the same prooftheoretic ordinal as well? What's a good reference for this?

2$\begingroup$ Goodstein's theorem is a true $\Pi^0_2$ statement not provable in any of these theories, but provable via finitistic means once we have $\epsilon_0$induction. This is explained in detail in Methamathematics of first order arithmetic. $\endgroup$– Andrés E. CaicedoJan 22, 2014 at 0:02
1 Answer
This is an instance of a general phenomenon: adding true $\Pi_1$ sentences to a reasonable theory doesn't change its prooftheoretic ordinal. $Con(T)$ is $\Pi_1$, so if $T$ is any consistent theory, $PA+Con(T)$ still has prooftheoretic ordinal $\epsilon_0$.
This is a standard fact in the area, though I'm not sure it's included in the usual sources on ordinal analysis. An easy way to see this is to notice that the usual cutelimination proof for $PA$ goes through essentially unchanged $PA+\sigma$ whenever $\sigma$ is $\Pi_1$ and true.
In general, $PA+\forall x\psi(x)$ doesn't have any new "computational" information when $\forall x\psi(x)$ is true. One would like to say that $PA+\forall x\psi(x)$ is conservative for "properly $\Pi_2$ formulas"$\Pi_2$ formulas which aren't just $\Pi_1$ formulas in disguise. One way to make this precise is: suppose $PA+\forall x\psi(x)\vdash\forall x\exists y\phi(x,y)$. There's a corresponding computable function $f$ so that for each $x$, $f(x)$ is least such that $\phi(x,f(x))$ holds. Then $\forall x\exists y\phi(x,y)$ is equivalent to $tot(f)$, the formula $\forall x\exists y f(x)=y$.
It need not be the case that $PA\vdash tot(f)$: if $PA\not\vdash\forall x\exists y\phi(x,y)$ and $\phi(x,y)$ is just $\psi(x)$ then $f$ is the function which checks whether $\psi(x)$ holds and outputs $0$ if so and runs forever if not. However there is always a related computable function $f'$ given as follows: on input $x$, if $f(x)$ terminates in $s$ steps and for each $i\leq s$, $\psi(i)$ holds, $f'(x)$ outputs $f(x)$; if there is an $s$ such that $\neg\psi(s)$ and $f(x)$ has not terminated in $s$ steps, $f'(x)$ outputs (say) $0$.
Then $PA\vdash tot(f')$, and, since $\forall x\psi(x)$ is true, $\forall x f(x)=f'(x)$. In particular, this means that adding true $\Pi_1$ formulas doesn't prove the totality of any functions which grow more quickly than those provably total in $PA$.
This is basically what we'd expect in a wellbehaved theory: adding (true) universal formulas shouldn't give new existential information. (A poorly behaved theory could have an axiom like $\sigma\rightarrow\forall x\exists y\phi$, so this isn't true in general.)

3$\begingroup$ Nice heuristic in the last paragraph. $\endgroup$ Jan 22, 2014 at 0:16

1$\begingroup$ Every $\Sigma_1$sound extension of PA (or Q, for that matter) is $\Sigma_1$conservative over PA, due to $\Sigma_1$completeness of Q. The only nontrivial fact here is that the conservativity is verifiable in a weaker theory. $\endgroup$ Jan 22, 2014 at 11:05

$\begingroup$ No, wait, that’s not true either. The $\Sigma_1$conservativity (or just relative consistency) of PA + Con(PA) over PA is even not provable in PA itself. So, the last paragraph is just a misleading reformulation of the fact that adding true $\Pi_1$ sentences preserves $\Sigma_1$soundness. Emphatically, this has nothing to do whatsoever with values of the prooftheoretic ordinals of the two theories in question. ZFC is $\Sigma_1$conservative over Q, despite having vastly different prooftheoretic strength. $\endgroup$ Jan 22, 2014 at 11:55

$\begingroup$ @EmilJeřábek: You're absolutely right. I was trying to simplify the actual statement about $\Pi_2$ formulas, and ended up simplifying down to something trivial. $\endgroup$ Jan 22, 2014 at 17:29

1$\begingroup$ @AndresCaicedo: This is a property of reasonableness of the theory, not its strength. You can easily extend PA, or a weaker theory like $I\Sigma_1$, to break these results (consider $T'=T+Con(PA)\rightarrow 1Con(PA)$; then $T'+Con(PA)$ has larger prooftheoretic ordinal). On the other hand these results hold for at least the usual theories we have cutelimination for (through $\Pi^1_2CA$). $\endgroup$ Jan 22, 2014 at 19:23