Logic · Arithmetic · Proof Theory
One and the same principle — "proved for the base and for the step ⇒ proved for all" — takes on substantially different logical forms depending on the language and the base theory: a countable axiom scheme in Peano arithmetic, a single second-order axiom in analysis, a theorem in set theory. This is a guide to these forms, their interrelations and boundaries; full statements and proofs are in the PDF.
Induction looks different not because mathematicians invent something new each time, but because the expressive power of the language changes: where quantification over sets is unavailable, one must make do with an axiom scheme — a separate axiom for each formula.
In the first-order language of arithmetic one can formulate five, at first glance, different principles. Some of them are equivalent to one another already in pure logic, without a single arithmetical axiom; another part requires minimal facts about the successor; the link to the last principle is the subtlest and metamathematically deepest. Three abbreviations everything rests on:
The three horizontal groups of the diagram are of fundamentally different natures: the left pair of arrows is a fact of pure logic (up to trichotomy of the order); the middle pair uses only minimal facts about the successor \(S\); the right pair already rests on the induction \(I\Delta_0\) and is proved noticeably harder (Paris–Kirby). Details of each transition — below and in the PDF.
A key observation: these three principles are equivalent to one another already in pure predicate calculus — without a single arithmetical axiom — provided only that \(<\) is a strict linear order (all that is needed is trichotomy: for any \(x,y\), exactly one of \(x{<}y\), \(x{=}y\), \(y{<}x\) holds).
(a) \(I^*_{\lnot\varphi}\iff D_\varphi\). The scheme \(I^*\) for the formula \(\lnot\varphi\) has the form \(A\to B\), where \(A\equiv\forall x(\forall y{<}x\,\lnot\varphi(y)\to\lnot\varphi(x))\), \(B\equiv\forall x\,\lnot\varphi(x)\). By the law of contraposition \(A\to B\iff\lnot B\to\lnot A\) — a pure tautology. Unfolding the negations by De Morgan's rules and quantifier duality, \(\lnot B\) is \(X\ne\varnothing\), and \(\lnot A\), after one more contraposition inside, is exactly \(\lnot(\forall x\in X\,\exists y\in X\,(y{<}x))\), i.e. the conclusion \(D_\varphi\).
(b) \(D_\varphi\iff L_\varphi\) — under trichotomy \(\lnot(y{<}x)\) means "\(y{=}x\) or \(x{<}y\)", i.e. exactly \(x\leqslant y\); the formulas \(D\) and \(L\), after unfolding the inner negation, coincide literally.
Since the class of formulas is closed under \(\varphi\mapsto\lnot\varphi\), it follows that the full schemes are equivalent: \(I^*\iff D\iff L\). Neither the number \(0\) nor the operation \(+1\) is used in the proof — only the linearity of \(<\).
The link of \(I\) with the triple \(I^*,L,D\) is of a different nature: it is inseparable from the successor \(S\) and therefore cannot be a purely logical fact. Three elementary axioms about how \(<\) and \(S\) fit together are needed (denote them (O1)–(O3); together with the recursive equations for \(+,\times,S\) they form the theory \(\mathsf{PA}^{\mathrm{rec}}_-\) — Robinson arithmetic in its original recursive form):
Lemma. From (O1)–(O3): \(\mathrm{Ind}(X)\to\mathrm{Prog}(X)\). Let \([0,x)\subseteq X\). By (O3) either \(x{=}0\) (then \(x\in X\) by the first conjunct of \(\mathrm{Ind}(X)\)), or \(x{=}Sz\): then by (O2) \(z{<}Sz{=}x\), so \(z\in[0,x)\subseteq X\), and by the second conjunct of \(\mathrm{Ind}(X)\) we get \(Sz{=}x\in X\).
\(I^*\Rightarrow I\). From \(\mathrm{Ind}(X)\), by the Lemma we get \(\mathrm{Prog}(X)\); applying \(I^*\), we obtain \(\mathrm{Tot}(X)\). Axiom (O3) is used here exactly once — in the case split "\(x\) is \(0\) or a successor".
\(I\Rightarrow I^*\) (without (O3)!). Let \(\mathrm{Prog}(X)\) hold. Define \(Y=\{x\mid[0,x)\subseteq X\}\) — the maximal initial interval inside \(X\). Then \(Y\subseteq X\) immediately by the definition of \(\mathrm{Prog}(X)\). Next, \(\mathrm{Ind}(Y)\): the base \(0\in Y\) — by (O1) \([0,0)=\varnothing\subseteq X\); the step — if \(z\in Y\), then \(z\in X\) (since \(Y\subseteq X\)), and by (O2) \([0,Sz)=[0,z)\cup\{z\}\subseteq X\), i.e. \(Sz\in Y\). Applying \(I\) to \(Y\), we get \(\mathrm{Tot}(Y)\), which together with \(Y\subseteq X\) gives the desired \(\mathrm{Tot}(X)\).
The asymmetry here is substantive: the direction \(I^*\Rightarrow I\) essentially uses all three axioms, with (O3) specifically used — in the case split; the direction \(I\Rightarrow I^*\) gets by with (O1)–(O2) and does not use (O3) at all. The model below shows this is not an accident.
Take as carrier the ordinal \(\omega+\omega\) — two consecutive copies of \(\mathbb N\) with the usual order, but define the successor separately within each copy: \(S(n)=n{+}1\) in the first, \(S(\omega{+}n)=\omega{+}n{+}1\) in the second. The function \(S\) is everywhere defined and injective, (O1)–(O2) hold — but the element \(\omega\) is not \(S(y)\) for any \(y\): this is exactly the point at which (O3) fails.
The set \(X\) = "first copy of \(\mathbb N\)" satisfies \(\mathrm{Ind}(X)\) (contains 0, closed under \(S\)), but \(X\ne\omega{+}\omega\) — so \(I\) fails for this \(X\). At the same time \(\omega+\omega\) is a genuine ordinal (a well-ordered set), so transfinite induction holds in it for arbitrary subsets of the carrier — so \(I^*\) (and with it \(L\), \(D\)) holds here, in a genuinely second-order sense, with no reservations about a scheme.
No: there exist nonstandard models of \(\mathsf{PA}\) in which the full scheme \(I\) (and with it \(I^*,L,D\) as schemes) holds, but the model itself, viewed from outside, is not well-ordered — it contains subsets (not definable in the language \(\mathsf{PA}\)) with no least element. There is no contradiction: as an axiom scheme, \(I^*\) guarantees a least element only for subsets definable by a formula of the language \(\mathsf{PA}\); the scheme simply does not extend to the "illegitimate" subsets of a nonstandard model. In the example above \(I^*\) was legitimately required for absolutely all subsets precisely because \(\omega+\omega\) is standard by construction.
The link of \(B\) with \(I\) reduces neither to pure logic nor to the minimal arithmetic of the successor. Inside the weak base theory \(\mathsf{PA}^-\) (the axioms of a discrete ordered semiring without induction), the scheme \(B\) on its own does not imply \(I\). But relative to the base induction \(I\Delta_0\), the link is restored and forms a strict hierarchy (Paris–Kirby, 1978):
while at the level of full schemes — \(I\iff B\) relative to the base \(I\Delta_0\). The proof of this transition is noticeably harder than the two previous ones and is not given in full here — it is worked out in full in the PDF.
Below is a set of statements whose provability is essentially tied to the strength of induction: some require only its weakest form, others are independent of the full scheme \(I\) of Peano arithmetic. The status is given in terms of arithmetic subsystems (\(I\Sigma_n\), \(I\Delta_0\)) and reverse mathematics (\(\mathsf{RCA}_0\), \(\mathsf{WKL}_0\), \(\mathsf{ACA}_0\), \(\mathsf{ATR}_0\)).
| Statement | Provability Status |
|---|---|
| Pigeonhole Principle |A|>|B| ⇒ no injection A→B | not in \(I\Delta_0\) Paris–Wilkie–Woods, Ajtai (1988): not provable even for \(\Delta_0\)-definable functions — demonstrating the extreme weakness of \(I\Delta_0\). |
| König's Lemma on Infinite Paths an infinite finitely-branching tree contains an infinite path | ≡ \(\mathsf{WKL}_0\) for binary trees (⇔ compactness of an interval); ≡ \(\mathsf{ACA}_0\) for arbitrary trees — strictly stronger. The difference arises not from induction (the scheme is the same in both systems), but from the comprehension scheme. |
| Commutativity and Associativity of \(+\), \(\times\) | Provable in \(\mathsf{PA}\) by induction. Without it (in \(\mathsf{PA}^{\mathrm{rec}}_-\)) there exist nonstandard models with noncommutative addition — as in ordinal arithmetic, where \(\omega{+}1\ne1{+}\omega\). |
| Dedekind-Finite Sets B⊊A finite ⇒ |B|<|A|; standard-finite ⇔ Dedekind-finite | The first is a direct consequence of induction. The direction "standard-finite ⇒ Dedekind-finite" — likewise. The converse requires countable choice \(\mathsf{AC}_\omega\) (only a consequence, not an equivalence); without choice in \(\mathsf{ZF}\) — unprovable (Fraenkel–Mostowski models, Cohen's first model give infinite Dedekind-finite sets). |
| Ramsey's Theorem \(RT^2_2\) finite case — the "party theorem," R(k,m); infinite — RT²₂ | The finite case — induction on \(k{+}m\). The infinite case — a direct consequence of the principle \(L\); exact strength \(\mathsf{RCA}_0{+}I\Sigma_2\), but \(RT^2_2\) itself does not imply \(I\Sigma_2\) (Cholak–Jockusch–Slaman, 2001). |
| Totality of the Ackermann Function | not in \(I\Sigma_1\) (Parsons's theorem: \(I\Sigma_1\)-provably-recursive functions = primitive recursive) → provable in \(I\Sigma_2\) — matching the place of the Ackermann function at level \(\omega\) of the fast-growing hierarchy. |
| Goodstein's Theorem (1944) and the Paris–Harrington Principle true \(\Pi_2\) and combinatorial sentences of the language \(\mathsf{PA}\) | not in \(\mathsf{PA}\) (Kirby–Paris, 1982; Paris–Harrington, 1977) — but already provable by transfinite induction along \(\varepsilon_0\) in \(\mathsf{ATR}_0\). The ordinal \(\varepsilon_0\) is the proof-theoretic ordinal of \(\mathsf{PA}\) (Gentzen, 1936): the boundary the scheme \(I\) cannot formalize on its own. |
The last row marks the limit of strength of local/course-of-values induction \(I\iff I^*\): for all the power demonstrated above, they are not closed under all true arithmetical statements. The Paris–Harrington principle is also notable for being the first example of a natural (not metamathematical in its statement) theorem whose independence from \(\mathsf{PA}\) was discovered simultaneously with the theorem itself.