Philosophy
The Logic of Second-Order Logic and Expressive Power
Quick fact
In second-order logic, the natural numbers can be characterized up to isomorphism—meaning all models of the Peano axioms are identical. This is impossible in first-order logic due to the Löwenheim–Skolem theorems, which force the existence of nonstandard models.
Why this is interesting
You know how we can say 'for all numbers' in logic? What if we could also say 'for all properties of numbers'? That simple change leads to a logic so powerful it can pin down the natural numbers exactly—but also breaks some of the most beloved properties of ordinary logic.
Read the full explanation
Understanding The Logic of Second-Order Logic and Expressive Power
Imagine you have a language where you can talk about individual objects, like numbers. That's first-order logic (FOL). Its variables range over objects. Now, imagine you can also talk about sets of objects, or relations between objects. You can say 'there exists a set of numbers that contains 0 and is closed under successor.' That's second-order logic (SOL). In FOL, you can't quantify over sets directly; you'd need an infinite axiom scheme. This extra ability lets SOL describe structures much more rigidly. For example, the second-order Peano axioms have only one model (up to isomorphism). But this power comes at a cost. FOL has a complete proof system: every logical truth is provable. SOL does not. Similarly, FOL satisfies compactness (if every finite subset of a theory is consistent, the whole theory is consistent) and the Löwenheim–Skolem property (if it has a model, it has a countable model). SOL fails both. So while SOL can express things FOL cannot, it loses the nice metatheoretic properties that make FOL mathematically manageable.
A deeper explanation
The deep reason for this trade-off lies in the nature of quantification. In FOL, quantifiers range over a fixed domain, and the semantics are simple: a sentence is true if it's satisfied in some structure. This simplicity allows a complete proof system, as shown by Gödel's completeness theorem. In SOL, quantifiers range over subsets of the domain, which vastly increases expressive power but also introduces semantic complexity. The truth of a second-order sentence may depend on the entire power set of the domain, which is not effectively enumerable. This is why no complete, sound, and effective proof system can exist for standard second-order logic (as follows from Tarski's theorem on the undefinability of truth). Furthermore, the compactness theorem fails because a set of sentences can be finitely satisfiable but not jointly satisfiable if it involves second-order quantification. The Löwenheim–Skolem theorem fails because second-order logic can express that a structure is uncountable, preventing existence of countable models when there is an uncountable one. These failures are not mere technicalities; they reflect a philosophical choice: FOL aligns with the idea of a formal system in which every true statement can be proved, while SOL seeks to express mathematical truths more directly, even if they elude proof. This connects to the foundational debates in mathematics, such as whether the continuum hypothesis is true or false in a 'standard' model. In fact, second-order logic can express the continuum hypothesis (CH) in a single sentence, because it can quantify over all sets of reals. Thus, while SOL is more expressive, it is also more sensitive to the underlying set-theoretic universe. This makes SOL a powerful tool for characterizing mathematical structures, but a less convenient one for a complete formal system.