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:
Has there been any research on this phenomena, e.g. in proof theory or in automated theorem proving?
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
$T \cup \{\phi(0) \wedge \forall x(\phi(x) \to \phi(S(x))) \to \forall x \phi(x)\} \not\vdash \forall x \phi(x)$,
$T \vdash \phi(0)$,
$T \vdash \psi(0)$,
$T \vdash \forall x(\psi(x) \to \psi(S(x)))$,
$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)$.
