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
    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$ 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$ 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
    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$ Jan 4, 2017 at 19:18


You must log in to answer this question.

Browse other questions tagged .