Formally what is the first and second order induction axiom?

Question

In formal logic notation how do you write the first order induction axiom and second order induction axiom as we might find them in Peano Arithmetic and what is the difference between them exactly?

Answer 1

First order:

For any first order formula $\phi$ in the language of arithmetic, the following is an axiom: $$ (\phi(0) \land\forall x(\phi(x)\to\phi(S x)))\to \forall x\phi(x).$$

Second order:

The following is an axiom: $$ \forall P((P(0)\land \forall x(P(x)\to P(x+1))\to \forall x P(x))$$

The first is infinitely many axioms (aka an axiom schema) whereas the second is a single axiom. So in the first, the “quantification over predicates” is something that happens externally whereas in the second the quantification can be expressed in the language. Also notice that in the first we only include predicates that can be expressed as an arithmetical formula. Whereas in the second we include any arbitrary predicate (assuming full semantics).

Note also there aren’t only two options. There are intermediate systems that include some second-order properties (mediated by comprehension axioms). There are also a whole bunch of induction principles weaker than first order induction.

---

Here is a standard example of using first order induction: say we want to prove every nonzero number has a predecessor. Well, "$x$ has a predecessor" is something we can write as a first order sentence in arithmetic: $x\ne 0\to \exists y (x=Sy).$ And so we can apply induction to it in first order PA. The statement holds vacuously for $x=0$ (base case) and if it holds for $x$ then it holds for $S x,$ since obviously $S x$ has a predecessor, namely $x$ (this is the induction step, although we didn't actually need to use the induction hypothesis). Thus we have proven in (first order) PA that every nonzero number has a predecessor.

---

Here's a famous example for full second order induction. We call a property "inductive" if it holds for zero, and is closed under successor, i.e. it satisfies the premise of the induction: $$ I(P) := P(0)\land \forall x(P(x)\to P(S x)).$$ So $I(P)$ is a second order sentence that means that $P$ is an inductive property. Now we want to show that any inductive property holds for all numbers, in other words $$ \forall x\forall P (I(P) \to P(x)).$$

Note that we are way far gone into second order territory now... we are not only writing down abstract property variables but quantifying over them.

We want to apply induction to the second order formula $$ \phi(x) = \forall P (I(P) \to P(x)).$$ But note the way we stated the induction principle, it applies to abstract properties, not to formulas. But not to worry: in (full) second order logic, we have a comprehension scheme that says any formula determines a property, i.e. for any $\phi,$ we have $\exists Q \forall x(Q(x)\leftrightarrow \phi(x)).$ So this gives us the rubber stamp to perform induction on a second order formula, since it's equivalent to some property.

So we proceed to prove it by induction. $\phi(0)$ holds since $P$ is inductive and therefore $P(0)$ holds. Now for the induction step we assume $\phi(x)$ holds and prove $\phi(S x).$ So we need to show for an arbitrary property $P$ that $I(P)\to P(S x),$ in other words that for an arbitrary inductive property $P(S x)$ holds. Well, we have as our induction hypothesis that $\forall P(I(P)\to P(x))$ so for an arbitrary inductive property, $P(x)$ holds, but since $P$ is inductive, this means $P(S x)$ holds.

So we've shown in second order arithmetic that any inductive property holds universally. The significance of this is that it means our domain must be the smallest possible inductive set, where an inductive set is one that contains our interpretation of $0$ and is closed under our interpretation of the $S$ function. (Since its elements have every inductive property, i.e. it is a subset of any other inductive set). This characterizes the structure up to isomorphism, so there is only one model of full second order arithmetic, namely the natural numbers with their usual successor relation.

This really goes above and beyond what we can show, or even express in the first order theory. In fact first order PA has many different models, as does any first order theory with infinite models. In fact we can say more: it has many different models with different first order properties, which is a consequence of Gödel’s incompleteness theorem for formal system combined with his completeness theorem for first order logic.