12
$\begingroup$

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?

$\endgroup$
1
  • 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. Caicedo Jan 22 '14 at 0:02
16
$\begingroup$

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

$\endgroup$
13
  • 3
    $\begingroup$ Nice heuristic in the last paragraph. $\endgroup$ – Andrés E. Caicedo Jan 22 '14 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$ – Emil Jeřábek Jan 22 '14 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 proof-theoretic ordinals of the two theories in question. ZFC is $\Sigma_1$-conservative over Q, despite having vastly different proof-theoretic strength. $\endgroup$ – Emil Jeřábek Jan 22 '14 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$ – Henry Towsner Jan 22 '14 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 1-Con(PA)$; then $T'+Con(PA)$ has larger proof-theoretic ordinal). On the other hand these results hold for at least the usual theories we have cut-elimination for (through $\Pi^1_2-CA$). $\endgroup$ – Henry Towsner Jan 22 '14 at 19:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.