What system suffices to show the strength of PRA is $\omega^\omega$?

Russell O'Connor wrote in 2009 (link):

PRA has consistency strength equivalent to the well-foundness of $$\omega^\omega$$, which can be stated again as the termination of some other program on all inputs. Presumably this equivalence is proved in a still weaker system.

Is this true? What is the weakest system that suffices to prove that well-foundedness of $$\omega^\omega$$ implies consistency of PRA? And is it truly weaker than PRA?

• I imagine Russell was going by the Wikipedia article: en.wikipedia.org/w/…. Maybe one of the references there has details. Jun 19 '19 at 1:21
• @Todd there are 5 books listed, plus papers :-) I'm not so invested in the question that I feel like digging through them all, given there is no specific citation. Jun 19 '19 at 6:13
• First, you need to decide what “well-foundedness” is. In particular, over any reasonable base theory (say, $\mathrm{PA}^-$, the theory of nonnegative parts of discretely ordered rings) and for a nonobfuscated definition of $\omega^\omega$, induction over $\omega^\omega$ implies induction over $\omega$, i.e., PA, which of course proves both PRA and its consistency. However, the result should hold (for nontrivial reasons) even for, say, quantifier-free induction over $\omega^\omega$ in a sufficiently rich language (say, with polynomial-time function symbols) over a similar base theory. Jun 19 '19 at 7:06
• David, sorry I wasn't more clear: in view of your question "is this true?", it was meant partly to deflect from the idea that it was Russell asserting it, to the idea that maybe he was just quoting Wikipedia. I agree it would be good to get an expert opinion. Jun 19 '19 at 11:34
• @Todd Ah, I see. Fair call. Jun 19 '19 at 13:41

First, this is not quite the right question. The implication as such is going to be provable in a trivial base theory; the most important question is what “well-foundedness of $$\omega^\omega$$” means in the statement. Well-foundedness is not directly expressible in the language of first-order arithmetic, it has to be approximated by the transfinite induction schema, and then the strength of the hypothesis is gauged by the complexity of formulas allowed in the induction schema.

Having said that, let $$\mathrm{PA}^-$$ be the theory of nonnegative parts of discretely ordered rings (see e.g. Wikipedia), which has the proof theoretic strength of Robinson’s $$Q$$ (much weaker than PRA).

By , $$\mathrm{PA}^-$$ is capable of basic sequence coding; let $$L^+$$ denote the usual language of arithmetic $$(+,{\cdot},0,1,{\le})$$ augmented with a function symbol $$(w)_i$$ for extracting the $$i$$th element of a sequence coded by $$w$$, and a relation symbol expressing “$$w$$ and $$w'$$ encode the same sequences, except possibly for the $$0$$th element”. Note that in the encoding scheme used in , fixed-length sequences $$(x_0,\dots,x_k)$$ are also computable by $$L^+$$-terms. Let $$\mathrm{Open}^+$$ denote the set of quantifier-free (= open) $$L^+$$-formulas, and let $$\mathrm{Open}^+\text-\mathrm{TI}_{\omega^\omega}$$ denote the transfinite induction schema $$\forall x\,\bigl(\forall y\,(y\prec x\to\phi(y))\to\phi(x)\bigr)\to\forall x\,\phi(x)$$ for $$\phi\in\mathrm{Open}^+$$. Here $$\prec$$ is the ordering relation of the natural definition of $$\omega^\omega$$ in arithmetic, whereby an ordinal with Cantor normal form $$\omega^mn_m+\omega^{m-1}n_{m-1}+\dots+\omega^0n_0$$ is represented by (a code of) the sequence $$(n_0,\dots,n_m)$$.

Theorem: $$\mathrm{PA}^-+\mathrm{Open}^+\text-\mathrm{TI}_{\omega^\omega}\vdash\mathrm{Con_{PRA}}$$.

In fact, $$\mathrm{PA}^-+\mathrm{Open}^+\text-\mathrm{TI}_{\omega^\omega}\equiv I\Sigma_1+\Pi_1\text-\mathrm{TI}_{\omega^\omega}.$$

The first assertion follows from the second, because $$I\Sigma_1+\Pi_1\text-\mathrm{TI}_{\omega^\omega}$$ is more than enough to comfortably formalize the standard proof of the consistency of PRA (or $$I\Sigma_1$$) by cut elimination, or alternatively, to carry out a model-theoretic proof of ordinal analysis, as presented in .

Now, to prove the second claim: first, since we can translate from natural numbers to the corresponding ordinals $$<\omega$$ and back by $$L^+$$-terms, it is easy to see that $$\mathrm{PA}^-+\mathrm{Open}^+\text-\mathrm{TI}_{\omega^\omega}$$ proves ordinary induction for $$\mathrm{Open}^+$$ formulas, and in particular, it includes the theory $$\mathrm{IOpen}$$. But we can do much better. The theory actually proves the least number principle for existential formulas, $$L\exists_1$$, and therefore also the induction schema for existential formulas, $$I\exists_1$$: to see this, let $$\phi(x)$$ be an existential formula of the form $$\exists y\,\theta(x,y)$$ where $$\theta$$ is open. Define an open formula $$\psi(\alpha)$$ so that $$\psi(\omega^1n+\omega^0m)\iff\theta(n,m).$$ By $$\mathrm{TI}_{\omega^\omega}$$ for the formula $$\neg\psi$$, or equivalently, the least element principle (wrt $$\omega^\omega$$) for $$\psi$$, if $$\exists x\,\phi(x)$$, then there exists a least $$\alpha=\omega n+m$$ such that $$\psi(\alpha)$$. Then $$\phi(n)$$, but $$\neg\phi(n')$$ for all $$n', as $$\omega n'+m'\prec\omega n+m$$ for any $$m'$$. Thus, $$n$$ is the least number satisfying $$\phi(n)$$.

By a similar argument, we can also prove the least element principle wrt $$\omega^\omega$$ for $$\exists_1$$ formulas, or dually, $$\forall_1\text-\mathrm{TI}_{\omega^\omega}$$, where $$\forall_1$$ denotes the set of universal formulas.

As shown in , $$I\exists_1$$ proves a form of the MRDP theorem: every $$\Sigma_1$$ formula is equivalent to an $$\exists_1$$ formula. In particular, $$I\exists_1\equiv I\Sigma_1$$, and $$I\exists_1+\forall_1\text-\mathrm{TI}_{\omega^\omega}\vdash\Pi_1\text-\mathrm{TI}_{\omega^\omega}$$.

References:

 Jeřábek, Emil, Sequence encoding without induction, Math. Log. Q. 58, no. 3, 244–248 (2012). ZBL1248.03079.

 Avigad, Jeremy; Sommer, Richard, A model-theoretic approach to ordinal analysis, Bull. Symb. Log. 3, no. 1, 17–52 (1997). ZBL0874.03068.

 Kaye, Richard, Diophantine induction, Ann. Pure Appl. Logic 46, no. 1, 1–40 (1990). ZBL0693.03038.

• So is it fair to say, sweeping some details under the rug, that something equivalent in strength to $Q$ proves that transfinite induction along $\omega^\omega$ (aka $\omega^\omega$ is well-founded) implies $\mathrm{Con}(\mathrm{PRA})$? Jun 19 '19 at 13:45
• Basically, yes. Jun 19 '19 at 13:46
• I would say that the concept of proof-theoretic ordinals falls apart for such weak theories. When I wrote that $\mathrm{PA}^-$ has the proof-theoretic strength of $Q$, I simply meant that it is interpretable in $Q$ (on a definable cut). But interpretability may also be a too crude measure of strength, as all theories between $Q$ and, say, $I\Delta_0+\Omega_1+B\Sigma_1$ are mutually interpretable. Jun 19 '19 at 14:03
• @AlecRhea There is an approach to this by Arnold Beckmann. He proposed certain adaptation of the notion of proof-theoretic ordinal for the context of bounded arithmetics called "dynamic ordinals". However, I don't know enough about that myself to really try to explain it. Jun 20 '19 at 6:36
• @AlecRhea What people do in practice in bounded arithmetic is to compare the strength of theories by their low-complexity fragments or the corresponding complexity-theoretic devices, such as the propositional proof systems that can be proven consistent in the theory (which describes the $\forall\Delta^b_1$ fragment) or the provably total NP-search problems of the theory (which corresponds to the $\forall\Sigma^b_1$-fragment modulo true $\forall\Delta^b_1$ sentences). Jun 20 '19 at 6:57