Philosophy
Second-Order Logic and the Expressive Power of Quantification
Quick fact
In second-order logic, you can write a single sentence that fully describes the natural number structure: any two models satisfying it are isomorphic. First-order logic can never do this—by the Löwenheim-Skolem theorem, any first-order theory with an infinite model has models of every infinite size.
Why this is interesting
What if, in addition to saying 'every frog is green,' you could also say 'there is a property that every green thing shares'? That leap—from talking about things to talking about their properties—explodes the limits of logical expression.
Read the full explanation
Understanding Second-Order Logic and the Expressive Power of Quantification
Imagine logic as a language. First-order logic (FOL) lets you talk about objects: 'For every x, if x is a frog, then x is green.' You can use variables for individual objects, and you can say 'for all' or 'there exists' about those objects. When you step up to second-order logic (SOL), you are allowed to quantify over properties of those objects: 'There exists a property P such that P is shared by all frogs.' This means you can say things like 'There is a relation that orders the numbers in a certain way' without having to specify that relation in advance. The extra expressive power lets you capture concepts like 'finite', 'well-ordering', or 'the natural numbers' in a single sentence. In FOL, you cannot do this—any attempt to pin down the natural numbers is met with nonstandard models (models that contain infinite descending chains, for instance). SOL gives you the power to rule out such unintended models: it can say 'there is no infinite descending chain' by quantifying over relations. This power is not free; we will soon see what it costs.
A deeper explanation
The price of SOL's expressive power is the loss of several key metatheoretic properties that FOL enjoys. In FOL, the Compactness Theorem holds: if every finite subset of a set of sentences has a model, then the whole set has a model. This fails in SOL. Similarly, the Löwenheim-Skolem theorem (which says that any first-order theory with an infinite model has a model of every infinite cardinality) fails in SOL—which is exactly why SOL can characterize structures like the naturals, whose models all have the same cardinality. More dramatically, the Completeness Theorem fails for SOL: although there is a sound and complete proof system for FOL (where being syntactically provable equals being semantically true in all models), no such system exists for SOL under its standard (full) semantics. This is a direct consequence of Gödel's incompleteness theorem: a complete proof system for SOL would let you derive all true arithmetic statements, impossible by Gödel. Under a different, 'Henkin' semantics that restricts what counts as a second-order domain, SOL can be made complete with respect to a kind of first-order model, but then it collapses to many-sorted first-order logic, losing its categoricity. This illustrates a central trade-off in logic: expressive power and semantic strength versus effective proof theory and model-theoretic tractability.