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
∀X	—	Second-order universal	For all properties X
∃X	—	Second-order existential	There exists a property X
X(t)	—	Predication	t has property X
∀x	U+2200	First-order universal	For all individuals
∃x	U+2203	First-order existential	There exists individual
⊆	U+2286	Subset	Property inclusion
P(D)	—	Power set	All subsets of domain

Metatheory. Full semantics: Completeness fails — no proof system captures exactly the valid formulas. Compactness fails. Löwenheim-Skolem fails. Categoricity possible: second-order PA has a unique model. Validity is not even arithmetically definable (beyond the arithmetic hierarchy). Henkin semantics: Completeness, compactness, Löwenheim-Skolem hold — essentially first-order logic in disguise. MSO over trees is decidable (Rabin 1969) — basis for tree automata and verification.

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. Under full semantics: no complete proof system, no compactness, highly undecidable. "Not really logic" critique: full second-order validity depends on set-theoretic assumptions. Henkin semantics is tractable but loses expressive power. MSO is decidable only on restricted structures. The philosophical status is contested: is quantifying over "all properties" well-defined?