How do we know PA is incomparable with PRA + $\epsilon_0$?

Gödel 2 says that no subtheory of PA can prove Con$$_{PA}$$, and even though most natural theories $$T$$ extending PA can prove Con$$_{PA}$$, this is relatively uninteresting since anyone doubting the consistency of PA would certainly mistrust $$T$$. If all "natural" theories were totally ordered that would be the end of it, but the significance of Gentzen's consistency proof is that it establishes Con$$_{PA}$$ from an incomparable system PRA + $$\epsilon_0$$, which one can conceivably believe in without already trusting PA in the first place.

To see that PRA + $$\epsilon_0 \not\subseteq$$ PA, is straightforward, since the latter proves induction up to $$\epsilon_0$$, Con$$_{PA}$$, and Goodstein's theorem, none of which PA can prove (if its consistent).

But showing PA $$\not\subseteq$$ PRA + $$\epsilon_0$$ has me scratching my head. Wikipedia claims the latter "does not prove ordinary mathematical induction for all formulae" which PA does by definition. But no justification or reference is given there, and it's not obvious to me (or my thesis advisor) how to prove this claim (assuming a metatheory that can prove its consistency and perhaps more).

I'm also interested if there are any other (ideally "natural") statements that PA proves but PRA + $$\epsilon_0$$ does not. I can think of very few that PA proves but PRA alone doesn't, and it seems these will necessarily involve fast-growing functions like Ackermann. So e.g. the totality of Ackermann is the classic example of something PA can prove but not PRA, but if I'm not mistaken that statement can also be shown by induction up to $$\omega^\omega$$ so it doesn't resolve this question. To summarize:

How do we rigorously show that PRA + $$\epsilon_0$$ does not prove PA's induction schema? Are there any other statements that have this property, and why?

• What do you mean by $\epsilon_0$? A schema of transfinite induction of length $\epsilon_0$? The statement that a certain linear order (of type $\epsilon_0$ is well-founded? Something else? – Andrés E. Caicedo Mar 7 at 20:47

This is far from optimal, but it is fun:

Note that PRA isn't literally in the same language as PA, so by "PRA" we really mean "an appropriate rephrasing of PRA in the language of PA." This isn't an issue in this context, but it's worth pointing out.

Let's shift attention. The theory $$I\Sigma_1$$ consists of basic arithmetic (the ordered semiring axioms) and induction for $$\Sigma_1$$-formulas. It's not hard to check that $$I\Sigma_1$$ contains PRA ($$I\Sigma_1$$ proves "every primitive recursive function is total").

So it's enough to show that "$$I\Sigma_1+\epsilon_0$$" doesn't contain PA. Why is $$I\Sigma_1$$ a better theory to use here? Well, it turns out that $$I\Sigma_1$$ is finitely axiomatizable. Hence $$I\Sigma_1+\epsilon_0$$ is also finitely axiomatizable.

• The key here: induction for bounded-complexity formulas along $$\epsilon_0$$ looks like a scheme, but can be captured by a single sentence via the appropriate truth-predicate. (Of course that breaks down if we drop "bounded" ...)

... So what? Well, this is the neat bit: there is a beautiful model-theoretic proof of the incompleteness of PA (due to Kripke, written up by Putnam) which has as a corollary that no finitely axiomatizable extension of PA in the language of PA is consistent (the key aspect of PA being that it proves the consistency of each of its finite subtheories). Bam, we're done.

• Wow, not the strategy I was expecting, and I learned a lot from that! Do you have justification/reference for why $I\Sigma_1$ is finitely axiomatizable? I'm quite ignorant about that. – Morgan Sinclaire Feb 28 at 22:22
• I assume you mean that you use partial truth predicates, i.e. a $\Sigma_2$ formula $Tr_1$ such that $Tr_1(\ulcorner \phi(x) \urcorner) \leftrightarrow \phi(x)$ is provable for (the Gödel number of) any $\Sigma_1$ formula $\phi$. But it's not clear to me how to use that to get a finite axiomatization. – Morgan Sinclaire Feb 28 at 22:29
• So I'm scrutinizing pp. 350-360 of Metamathematics of First-Order Arithmetic. It'll take me some time to digest but p. 353 says "$I\Delta_0$ is not finitely axiomatizable". Which makes me skeptical of your claim, or at least if would be interesting if true. – Morgan Sinclaire Feb 28 at 22:44
• @MorganSinclaire Remember that $\Delta$ and $\Sigma$ are very different - roughly, the set of $\Sigma_n$ formulas is computable but the set of $\Delta_n$ formulas isn't (remember that $\Delta_n$ isn't a syntactic condition, it's a semantic one - it asserts equivalence with both a $\Sigma_n$ and $\Pi_n$ formula). For our purposes, remember that there is a "universal" $\Sigma_1$ formula, and we can use this to get a single sentence asserting that all instances of $\Sigma_1$-induction hold. (I'm a bit busy at the moment, details in a bit.) – Noah Schweber Feb 28 at 23:02
• Ah, p. 78 does show that $I\Sigma_n$ is finitely axiomatizable for n > 0, and it uses partial truth predicates as you said. – Morgan Sinclaire Feb 28 at 23:06