Second-Order Logic
Origin. Implicit in Frege's Grundgesetze (1893). Explicitly developed through work on foundations of mathematics. David Hilbert and Wilhelm Ackermann distinguished first and second order (1928). Debates about its status: is it really "logic" or disguised set theory? Quine skeptical; Boolos and others defended it.
Models. Quantification over predicates and relations, not just individuals. "There exists a property P such that..." Can express concepts first-order logic cannot: finiteness, transitive closure, mathematical induction. More expressive but less well-behaved.
Formalism.
Syntax: First-order logic extended with:
- Predicate variables: X, Y, Z, ... (ranging over properties/relations)
- Quantification over predicates: ∀X, ∃X
Examples:
- Leibniz's law: ∀x∀y(x = y ↔ ∀X(X(x) ↔ X(y)))
- Induction: ∀X((X(0) ∧ ∀n(X(n) → X(n+1))) → ∀nX(n))
- Finiteness is second-order expressible
Semantics:
- Full semantics: Predicate variables range over ALL subsets/relations on the domain. Second-order quantifiers are true power-set quantifiers.
- Henkin semantics: Predicate variables range over a designated collection of subsets/relations (not necessarily all). Behaves more like first-order logic.
Full second-order logic:
- M ⊨ ∀Xφ iff for all S ⊆ Dⁿ, M[X↦S] ⊨ φ
- Categoricity possible: full second-order Peano arithmetic has exactly one model (ℕ)
Monadic second-order (MSO): Quantify only over unary predicates (sets), not relations. Decidable over certain structures (trees, words).
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| ∀ | U+2200 | Universal quantifier | Binds individual variables (∀x) or predicate variables (∀X) |
| ∃ | U+2203 | Existential quantifier | Binds individual variables (∃x) or predicate variables (∃X) |
| X, Y, Z | — | Predicate variables | Range over properties and relations on the domain |
| x, y, n | — | Individual variables | Range over the domain |
| X(t) | — | Predication | The individual denoted by t falls under X |
| ⊆ | U+2286 | Subset of or equal to | Relation between a predicate's extension and the domain |
| ⊨ | U+22A8 | True / Satisfies | Satisfaction in a structure |
| ↦ | U+21A6 | Maps to | Variable reassignment, as in M[X↦S] |
| ↔ | U+2194 | Biconditional | Used in Leibniz's law |
| → | U+2192 | Conditional | Used in the induction axiom |
| ∧ | U+2227 | Conjunction | Used in the induction axiom |
| = | U+003D | Identity | Defined second-order by Leibniz's law |
| ℕ | U+2115 | Double-struck capital N | The natural numbers, categorically characterized second-order |
| ℝ | U+211D | Double-struck capital R | The reals as the complete ordered field |
| κ | U+03BA | Small letter kappa | An inaccessible cardinal, in Zermelo's quasi-categoricity theorem |
| P(D) | — | Power set | All subsets of the domain D |
| V_κ | — | Cumulative hierarchy stage | The models of second-order ZFC |
| S | — | Relation on the domain | The value assigned to a predicate variable, S ⊆ Dⁿ |
| M | — | Structure | With domain D |
| MSO | — | Monadic second-order logic | The fragment quantifying over sets only |
| S2S | — | Second-order theory of two successors | The MSO theory of the infinite binary tree; decidable by Rabin |
Metatheory. The two semantics have opposite metatheories, and which one is meant decides every question. Under full semantics categoricity is available — Dedekind's characterization of ℕ and Huntington's of the ordered field ℝ are second-order categorical, and Zermelo (1930) proved second-order ZFC quasi-categorical, its models being exactly the V_κ for inaccessible κ — but completeness, compactness and both Löwenheim–Skolem theorems all fail, and the failure is not marginal: the set of validities is not recursively enumerable, not arithmetical, and not definable in the analytical hierarchy, since truth in the standard model of arithmetic is second-order definable and Tarski's undefinability theorem then applies. Under Henkin semantics (1950), where predicate variables range over a designated collection closed under comprehension, all three classical theorems return, because the logic is then a two-sorted first-order theory. Between the two lies the monadic fragment, decidable over restricted structures: Büchi (1962) for infinite words and Rabin (1969) for the infinite binary tree, S2S, from which decidability of most modal and temporal logics is derived.
Applies to. Foundations of mathematics (categorical characterizations). Finite model theory. Descriptive complexity (captures PH). MSO in verification (tree automata, WS1S/WS2S). Philosophical logic (defining identity, natural numbers).
Limitations. The expressive power and the bad behaviour are the same fact. Under full semantics there is no complete effective proof system, since validity is not recursively enumerable and is not even definable in the analytical hierarchy; compactness and both Löwenheim–Skolem theorems fail; and the deductive calculus with comprehension that everyone actually uses is sound but incomplete, so second-order derivability and second-order consequence come apart permanently. The "disguised set theory" objection has a precise form: there is a second-order sentence that is valid exactly if the continuum hypothesis holds, so what counts as second-order valid is not settled by ZFC and varies with the background set theory — the logic does not have a determinate consequence relation unless set theory does. Switching to Henkin semantics restores completeness, compactness and Löwenheim–Skolem, but does so by readmitting the non-standard models, so categoricity for arithmetic and analysis is lost and the logic becomes a many-sorted first-order theory. Decidability is available only in the monadic fragment and only over restricted structures such as words and trees.
© 2026 Lingenic LLC