My questions are about the phenomenon that in order to prove a fact $\forall x \phi(x)$ by induction, sometimes straightforward induction "does not work" and instead one "must" use a "stronger" induction hypothesis $\psi(x)$, i.e. prove $\forall x \psi(x)$ by induction and then prove $\forall x \psi(x) \to \forall x \phi(x)$.

Several examples of this phenomenon: Strengthening the Induction Hypothesis

My two questions are:

  1. Has there been any research on this phenomena, e.g. in proof theory or in automated theorem proving?

  2. How would one formally state and prove/disprove that a fact $\forall x \phi(x)$ must be proved via a stronger induction hypothesis?

As for question 1 I have not been able to find anything, only a 1999 post on the FOM mailing list asking similar questions: https://www.cs.nyu.edu/pipermail/fom/1999-February/002660.html

As for question 2 here is an attempted formulation in the context of first-order arithmetic. I have not explored it further. In particular I have not investigated whether it applies to any of the natural cases of proof by strengthened induction hypothesis.

Let $\mathsf{Th}(\mathcal N)$ be true first-order arithmetic, i.e. the first-order theory of the structure $\langle \mathbb N, 0, +, \cdot, S \rangle$. Let $Q$ be the axioms of Robinson arithmetic in this language. Let $T$ be a theory such that $Q \subseteq T \subseteq \mathsf{Th}(\mathcal N)$. Let $\phi(x)$ and $\psi(x)$ be formulas both with at most one free variable $x$. Say that $\psi(x)$ witnesses that $T$ proves $\forall x \phi(x)$ with and only with strengthened induction hypothesis if and only if

  1. $T \cup \{\phi(0) \wedge \forall x(\phi(x) \to \phi(S(x))) \to \forall x \phi(x)\} \not\vdash \forall x \phi(x)$,

  2. $T \vdash \phi(0)$,

  3. $T \vdash \psi(0)$,

  4. $T \vdash \forall x(\psi(x) \to \psi(S(x)))$,

  5. $T \vdash \forall x \psi(x) \to \forall x \phi(x)$.

The motivation of these clauses is the following. Clause 3 says that $T$ and induction with $\phi$ as induction hypothesis does not work. Clause 4 ensures that this is because the inductive step fails. Clauses 5 and 6 ensures that $T$ and induction with $\psi$ as induction hypothesis proves $\forall x \psi(x)$, from which clause 7 gives $\forall x \phi(x)$.

  • $\begingroup$ Clause 3 would be a counterexample to induction, so I don't think that's what you want. I think instead you want the failure of T to prove the inductive step. $\endgroup$
    – user44143
    Commented Jan 4, 2017 at 17:59
  • $\begingroup$ What do you mean by counterexample to induction? Do you mean $T \vdash \lnot (\phi(0) \wedge \forall x(\phi(x) \to \phi(S(x))) \to \forall x \phi(x))$? I do not see how that follow from clauses 3–7. $\endgroup$ Commented Jan 4, 2017 at 18:12
  • $\begingroup$ As for failure of $T$ to prove the inductive step, i.e. $T \not\vdash \forall x(\phi(x) \to \phi(S(x)))$, that follows from these clauses. I guess clause 3 can be replaced by that. $\endgroup$ Commented Jan 4, 2017 at 18:15
  • 1
    $\begingroup$ A stupid remark: if $\forall n.\phi(n)$ is provable, then it can always be proven by induction on $\phi$, if in a very stupid/legalistic way: from $\forall n.\phi(n)$ we can deduce $\phi(0)$ as well as $\forall n.(\phi(n)\Rightarrow\phi(Sn))$ and then use these to prove $\forall n.\phi(n)$ by induction (forgetting or ignoring the fact that it has been proved in passing). So to make sense of your question, you'll have to make sense of "proving $X$ without proving $Y$ first", which seems very difficult. $\endgroup$
    – Gro-Tsen
    Commented Jan 4, 2017 at 19:12
  • 1
    $\begingroup$ @Gro-Tsen, indeed. Making sense of "Proving $X$ without proving $Y$ first" or "$Y$ must be proved before $X$" for arbitrary $X$ and $Y$ seems very difficult. My hope was that the special case of induction with strengthened induction hypothesis is simpler to deal with. $\endgroup$ Commented Jan 4, 2017 at 19:18


Your Answer

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

Browse other questions tagged or ask your own question.