6
$\begingroup$

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)

Improve this question
$\endgroup$
2
  • 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$
    – Gerry Myerson
    Commented 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
    Commented Jan 6, 2019 at 0:00

2 Answers 2

Reset to default
11
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 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
    Commented Jan 8, 2019 at 0:38
  • 1
    $\begingroup$ @LSpice yes that is correct $\endgroup$
    – Anders Lundstedt
    Commented Jan 8, 2019 at 11:15
6
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • $\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
    Commented 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$
    – Joel David Hamkins
    Commented 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$
    – Joel David Hamkins
    Commented 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
    Commented 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$
    – Anders Lundstedt
    Commented Jan 9, 2019 at 11:13

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .