Second-Order Logic

Definition

Second-order logic extends first-order logic by allowing quantification not only over individual elements of a domain, but also over properties, relations, and sometimes functions on that domain. Where first-order logic can say “for every element x”, second-order logic can say “for every property X” or “for every relation R.”

Why It Matters

Second-order logic is a high-expressivity background language for mathematics, finite model theory, automata, and verification. It can state principles such as induction and completeness as single structural axioms, but that expressive power comes with a semantic fork: full semantics supports categoricity-style claims, while Henkin/general semantics supports first-order-like proof theory.

Formalism / Key Objects

• Individual variables range over M.
• An n-ary relation variable X ranges, under full semantics, over subsets of M^n.
• Function variables range over maps M^n -> M.
• A typical second-order induction schema can be stated as one formula:

$$\forall X\left((X(0)\wedge \forall y(X(y)\to X(y^{+})))\to \forall yX(y)\right).$$

• A relation-comprehension instance has the form:

$$\exists R\forall x_1\dots x_n(\varphi (x_1,\dots ,x_n)\leftrightarrow R(x_1,\dots ,x_n)).$$

• Monadic second-order logic restricts relation variables to unary predicates. MSO over words and trees is central to automata-theoretic logic.
• Full and Henkin Second-Order Semantics records the semantic clauses and the full-vs-general-model tradeoff.

Connections

• Higher-Order Logic extends the same idea to variables over objects of lower types, including relations of relations.
• Automata-Theoretic Logic uses MSO as a bridge between logical definability and automata recognition.
• MSO Automata Correspondence is the wiki’s compact finite-word theorem-schema note for the regular-language/MSO equivalence.
• Linear Temporal Logic and other temporal logics often sit near automata/MSO translations, even when the user-facing specification language is not itself written as MSO.
• Formal Methods uses second-order expressivity in specification, synthesis, descriptive complexity, and proof-theoretic background.

Common Confusions

• Second-order logic is not just first-order logic with more predicates in the vocabulary; it adds quantification over predicates or relations themselves.
• Full and Henkin semantics are not minor implementation choices. They change which metatheorems hold and whether categoricity claims survive.
• MSO is a restricted second-order fragment, but in automata theory that restriction is often exactly what makes decision procedures possible.
• Second-order logic and set theory are related but not identical foundations: second-order quantifiers range over powers of a fixed domain, while set theory has a cumulative universe of sets.

Key Sources

• Vaananen2024 - Second-Order and Higher-Order Logic
• Hofmann2025 - Automata Theory and Logic
• Full and Henkin Second-Order Semantics