Is mathematical induction the only known example of a higher-order logic?

Question

Mathematical induction is one well known and widely cited example of a second-order logic.

I was wondering whether there are other examples of arguments involving higher-order logic in any branch of mathematics (well, except the formal logic itself, where examples would be trivial)?

Answer 1

The induction you are referring to is the (single) second-order induction axiom for second-order Peano Arithmetic, which says: $\def\imp{\Rightarrow}$

"$\forall pred\ P\ ( P(0) \land \forall n\ ( P(n) \imp P(n+1) ) \imp \forall n\ ( P(n) ) )$"

and this is of course how most people think of induction (and is also the original formulation by Peano). This is second-order because it quantifies over predicates, which is not allowed in first-order logic. There is another formal system called first-order Peano Arithmetic, and in logic this is what is called PA. Of course PA has no second-order induction axiom, but instead has a whole set of first-order axioms, one for each first-order predicate, which is called an induction schema:

"$P(0) \land \forall n\ ( P(n) \imp P(n+1) ) \imp \forall n\ ( P(n) )$" for any first-order predicate $P$.

The difference is crucial. There are at least two possible second-order semantics. Commonly second-order logic is interpreted with full semantics, where quantification over predicates ranges over all possible predicates, even if the predicate cannot be expressed by a formula. The second-order induction axiom then is extremely powerful, because it essentially ranges over the entire powerset of natural numbers. In contrast the first-order axiom schema only has countably many axioms, and so it 'controls' only countably many predicates and does not 'really know' the whole powerset, or in other words it 'only sees' the definable sets of natural numbers.

One might think that perhaps the distinction does not matter, but that is simply false. Second-order Peano Arithmetic is categorical, meaning that there is a unique model up to isomorphism. First-order Peano Arithmetic (PA) on the other hand is not even countably-categorical, meaning that it is not true that there is a unique countable model up to isomorphism. In fact, it can be shown (by using the compactness theorem) that there are uncountably many countable models of PA!