Second-Order Logic

Second-order logic is an extension of first-order logic that permits quantification not only over individual objects but also over properties and relations of those objects, and, in some formulations, over functions. Its distinctive feature is therefore the range of its variables, not the number of quantifiers in a formula. The same second-order language can receive different interpretations: full semantics gives it substantially greater expressive power than first-order logic, while Henkin semantics supports a complete effective deductive calculus. (math.uchicago.edu)

Syntax and quantification

First-order variables, conventionally written $x,y,z$, range over elements of a domain. Second-order variables, often written $X,Y,R$, range over properties or relations. A unary relation is interpreted as a subset of the domain; a binary relation as a set of ordered pairs; and an $n$-ary relation as a set of $n$-tuples. Relation variables have specified arities. (math.uchicago.edu)

For example,

says that there is a property $X$ holding of exactly those objects satisfying $P$. By contrast, in the first-order formula $\forall x\,P(x)$, $P$ is a fixed predicate symbol: the formula quantifies over objects, not over alternative interpretations of $P$. (plato.stanford.edu)

Some presentations also include variables ranging over functions. Function quantification can instead be represented through relation variables describing function graphs, with conditions ensuring a unique output for every input. Third-order and higher-order languages extend this arrangement further, allowing quantification over properties of properties or other higher-type objects. (plato.stanford.edu)

Full semantics and Henkin semantics

The interpretation of second-order quantifiers is the central dividing point between two approaches.

Under full semantics, also called standard semantics, a unary variable ranges over the entire power set $\mathcal P(D)$ of the individual domain $D$. An $n$-ary relation variable ranges over all subsets of $D^n$. Thus “every property” includes properties that cannot be defined by any formula in the language. (mv.helsinki.fi)

Under Henkin semantics, each relation type has a specified collection of admissible relations, which need not contain every relation on the domain. The interpretation of these collections forms part of the model. Consequently, a universal second-order statement may hold in a Henkin model because it holds for all available properties, even though it fails when every subset is available. (mv.helsinki.fi)

Terminology varies: arbitrary restricted-domain interpretations are often called general models, while Henkin models may specifically mean general models satisfying a chosen collection of comprehension and other axioms. A typical comprehension principle has the form

where $X$ is not free in $\varphi$. It ensures that the property expressed by $\varphi$ is available. Such principles do not by themselves force the available properties to be the full power set. (mv.helsinki.fi)

Henkin semantics can be represented using many-sorted first-order logic, with separate sorts for individuals and relations and predicates for relation application. This translation underlies its completeness and other first-order-like properties. (ps.uni-saarland.de)

Induction and categorical axiomatization

A principal mathematical application is the expression of induction in a single axiom. For a constant $0$ and successor function $S$, the second-order induction axiom is

It states that every property containing zero and closed under successor holds throughout the domain. Combined with the remaining Peano axioms, it characterizes the natural numbers up to isomorphism under full semantics. This property is called categoricity. (ps.uni-saarland.de)

First-order arithmetic instead uses an axiom schema of induction, with an instance for each formula. Under Henkin semantics, second-order induction also ranges only over available properties; it therefore does not guarantee the same external categoricity. (plato.stanford.edu)

Full second-order axioms can similarly characterize the real numbers as a complete ordered field: the least-upper-bound condition quantifies over all nonempty bounded subsets. These examples explain the importance of full semantics for specifying intended mathematical structures. (plato.stanford.edu)

Validity, completeness, and compactness

For unrestricted full semantics, the set of logically valid second-order sentences is not recursively enumerable. There is no sound, effective proof calculus deriving exactly all such validities. This is stronger than merely saying that validity is undecidable: first-order validity is also undecidable, but first-order logic has an effective complete calculus. (ps.uni-saarland.de)

Categoricity does not remove Gödel’s incompleteness phenomenon. It fixes the intended structure semantically, but does not supply an effective procedure proving every truth about that structure. Semantic determination and effective provability are different requirements. (ps.uni-saarland.de)

Under Henkin semantics, suitable calculi are sound and complete. The compactness theorem and Löwenheim–Skolem theorems also transfer through the first-order translation. Under full semantics, their usual first-order forms fail. (ps.uni-saarland.de)

An illustrative compactness counterexample uses full second-order Peano axioms together with a constant $c$ and the sentences

Every finite selection is satisfiable by choosing a sufficiently large natural number for $c$. The entire collection is unsatisfiable, because categoricity leaves no element distinct from every numeral. This construction combines categoricity with the definition of compactness. (ps.uni-saarland.de)

Fragments and computational applications

Monadic second-order logic restricts second-order variables to unary relations, or sets of individuals, while allowing fixed relations such as ordering. On finite words represented as ordered positions with letter predicates, it defines exactly the regular languages. The effective correspondence with finite automata provides decision procedures and a foundation for applications in formal verification. Decidability here concerns a specified class of structures, not unrestricted second-order logic. (arxiv.org)

Existential second-order logic consists of sentences of the form

where $\varphi$ is first-order. Fagin’s theorem, published in 1974, states that over finite relational structures, properties definable in this fragment are exactly those in the complexity class NP, under standard encodings. This is a foundational connection between logical definability and computational complexity. (arxiv.org)

For example, graph three-colorability can be expressed by existentially choosing three sets of vertices and requiring, using first-order conditions, that they partition the vertices and that no edge has both endpoints in the same set. Second-order quantification supplies a candidate certificate; the first-order part checks its conditions. (arxiv.org)

History and foundational questions

Gottlob Frege introduced second-order quantification in Begriffsschrift in 1879 and used the term “second order” in 1884. Leon Henkin’s 1950 work established completeness for a generalized interpretation of higher-order languages, making the distinction between full and general semantics fundamental to subsequent study. (plato.stanford.edu)

Foundational discussion concerns the status of quantification over all properties and the mathematical assumptions needed to interpret it. Full semantics is commonly defined within set theory, so its expressive strength relies on a background understanding of sets. Henkin semantics makes effective deduction available but does not generally preserve full-semantic characterizations of intended infinite structures. The choice between them changes the relationship among expressiveness, models, and proof, rather than merely changing notation. (mv.helsinki.fi)

References

1. Second-order and Higher-order Logicplato.stanford.edu
2. A Logical Insight into the Theory of Computationmath.uchicago.edu
3. Second-order logicmv.helsinki.fi
4. Undecidability, Incompleteness, and Completeness of Second-Order Logic in Coqps.uni-saarland.de
5. Completeness in the theory of typescir.nii.ac.jp
6. Lecture Notes on Monadic First- and Second-Order Logic on Stringsarxiv.org
7. Existential Second-Order Logic Over Graphs: A Complete Complexity-Theoretic Classificationarxiv.org