What is the proof-theoretic ordinal of PA + Con(PA), PA + Con(PA + Con(PA)) etc., and why?

Question

I seem to remember having read that the proof-theoretic ordinal (sup of ordinals the theory can prove well-ordered) 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 proof-theoretic ordinal as well? What's a good reference for this?

Answer 1

This is an instance of a general phenomenon: adding true $\Pi_1$ sentences to a reasonable theory doesn't change its proof-theoretic ordinal. $Con(T)$ is $\Pi_1$, so if $T$ is any consistent theory, $PA+Con(T)$ still has proof-theoretic 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 cut-elimination 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 well-behaved 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.)