# Cases where multiple induction steps are provably required

I am looking for references for theorems of the form:

1) Any proof of theorem $$X$$ requires $$n$$ applications of induction axioms

and especially

2) Any proof of theorem $$X$$ requires $$n$$ nested applications of induction axioms.

I've seen similar statements for applications of axioms other than induction axioms (and I'd be happy to receive references for those, too, but I am particularly interested in induction)

• If you can find a theorem that requires one induction, and a proof that if there's a theorem that requires $n$ inductions, then there's a theorem that requires $n+1$ inductions, then you're done! – Gerry Myerson Jan 5 '19 at 23:40
• I'm not sure this is possible: any (finite!) conjunction of instances of the Peano induction axioms can probably be derived from a single instance with a carefully chosen induction hypothesis. Or maybe it makes sense in certain axiomatic systems but not first-order Peano. A better measure of induction complexity is the quantifier depth hierarchy of the induction hypothesis. – Gro-Tsen Jan 6 '19 at 0:00

Here is a reference for one way of making precise sense of your question and answering it:

Stefan Hetzl and Tin Lok Wong (2017): "Some observations on the logical foundations of inductive theorem proving", Logical Methods in Computer Science, Volume 13, Issue 4, doi:10.23638/LMCS-13(4:10)2017, arXiv:1704.01930

In Section 2.4 they show the following. Let $$\text{PA}^-$$ be the theory of the non-negative parts of discretely ordered rings (language: $$\langle 0,1,+,\times,<\rangle$$—see the paper for an axiomatization). Then for each theorem $$\sigma$$ of PA there is a formula $$\varphi(x)$$ such that $$\text{PA}^-$$ proves $$\varphi(0)$$ and $$\forall x(\varphi(x)\implies\varphi(x+1))$$ and $$\forall x.\varphi(x)\implies\sigma$$. Thus in this sense one application of induction always suffices.

• Just to be totally clear, the parentheses in $\forall x.\varphi(x) \implies \sigma$ are $(\forall x.\varphi(x)) \implies \sigma$, right? – LSpice Jan 8 '19 at 0:38
• @LSpice yes that is correct – Anders Lundstedt Jan 8 '19 at 11:15

Here is an answer concerning recursion, rather than induction, but they are of course related.

Namely, the Ackermann function is defined by a double nested recursion $$A(m+1,n+1)=A(m,A(m+1,n))$$ with anchor cases defining $$A(0,n)$$ and $$A(m,0)$$. The function exhibits extremely rapid growth.

I mention the function because one can prove that the Ackermann function is not a primitive recursive function, which are the functions one can construct from some primitive functions by closing under composition and simple recursion.

Thus, the Ackermann function can be defined by a nested recursion, but not by a simple recursion.

• Obviously there are different senses of what it means to "require $n$ applications of induction axioms", but @AndersLundstedt argues elsewhere that, in some sense, one can always get away with one application of induction. Are you able to speak how this sense of induction-counting squares with the primitive-recursive sense? Does your sense allow distinguishing, say, functions requiring only doubly nested recursions from those requiring triply nested recursions? – LSpice Jan 8 '19 at 14:56
• PA proves that the Ackermann function is total, and this needs at most one instance of simple induction. Concerning the triple nesting idea, that is very interesting, and I am unsure about whether there is a triple nested version of the Ackermann function, which would not be amongst the functions you can get from the primitive functions using only double nested recursions. I imagine something like $B(r+1,s+1,t+1)=B(r,B(r+1,s,B(r+1,s+1,t)),B(r+1,s+1,t))$. – Joel David Hamkins Jan 8 '19 at 16:24
• It seems to me to be very likely that one could prove by a similar means as in the Ackermann function case that the individual levels of such a $B$ function eventually dominate every function that is definable by only a double nested recursion. – Joel David Hamkins Jan 8 '19 at 17:11
• There is a proof that the Ackermann function is definable in PA, which I believe requires nested induction (certainly induction over $\Sigma_2$ formulae). This seems to contradict Ander's answer... What am I missing? – cody Jan 9 '19 at 1:48
• @cody A "natural" proof might use nested induction, or at least more than one induction axiom. This does not contradict that one carefully chosen (but perhaps not very "natural") induction axiom would suffice. – Anders Lundstedt Jan 9 '19 at 11:13