Russell O'Connor wrote in 2009 ([link](http://r6.ca/blog/20091101T231201Z.html)):



> 
> 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?



What system suffices to show the strength of PRA is $\omega^\omega$?
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](https://en.wikipedia.org/wiki/Peano_axioms#Equivalent_axiomatizations)), which has the proof theoretic strength of Robinson’s $Q$ (*much* weaker than PRA).


By [1], $\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 [1], 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 [2].


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'<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 [3], $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:**


[1] *Jeřábek, Emil*, [**Sequence encoding without induction**](http://dx.doi.org/10.1002/malq.201200013), Math. Log. Q. 58, no. 3, 244–248 (2012). [ZBL1248.03079](https://zbmath.org/?q=an:1248.03079).


[2] *Avigad, Jeremy; Sommer, Richard*, [**A model-theoretic approach to ordinal analysis**](http://dx.doi.org/10.2307/421195), Bull. Symb. Log. 3, no. 1, 17–52 (1997). [ZBL0874.03068](https://zbmath.org/?q=an:0874.03068).


[3] *Kaye, Richard*, [**Diophantine induction**](http://dx.doi.org/10.1016/0168-0072(90)90076-E), Ann. Pure Appl. Logic 46, no. 1, 1–40 (1990). [ZBL0693.03038](https://zbmath.org/?q=an:0693.03038).


