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)

  • 6
    $\begingroup$ 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! $\endgroup$ Jan 5, 2019 at 23:40
  • 5
    $\begingroup$ 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. $\endgroup$
    – Gro-Tsen
    Jan 6, 2019 at 0:00

2 Answers 2


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.

  • 1
    $\begingroup$ Just to be totally clear, the parentheses in $\forall x.\varphi(x) \implies \sigma$ are $(\forall x.\varphi(x)) \implies \sigma$, right? $\endgroup$
    – LSpice
    Jan 8, 2019 at 0:38
  • 1
    $\begingroup$ @LSpice yes that is correct $\endgroup$ Jan 8, 2019 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.

  • $\begingroup$ 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? $\endgroup$
    – LSpice
    Jan 8, 2019 at 14:56
  • 2
    $\begingroup$ 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))$. $\endgroup$ Jan 8, 2019 at 16:24
  • $\begingroup$ 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. $\endgroup$ Jan 8, 2019 at 17:11
  • $\begingroup$ 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? $\endgroup$
    – cody
    Jan 9, 2019 at 1:48
  • 1
    $\begingroup$ @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. $\endgroup$ Jan 9, 2019 at 11:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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