Second-order and Higher-order Logic

Summary

This partial ingest covers Jouko Vaananen’s Stanford Encyclopedia of Philosophy entry on second-order and higher-order logic. The entry is useful as the wiki’s background source for why second-order quantification is both powerful and delicate: it can state categoricity-style axioms for familiar structures under full semantics, but that power depends on a set-theoretic metatheory and does not come with first-order-style completeness.

The note also routes the computer-science side of the entry: monadic second-order logic over words, trees, and finite structures connects directly to automata-theoretic methods, decidability, and descriptive complexity.

Key Claims

• Second-order logic extends first-order logic by adding variables and quantifiers for properties, relations, and functions over a domain.
• Full second-order semantics lets formulas quantify over all subsets, relations, and functions of the relevant arity, enabling categorical axiomatizations such as second-order induction for the natural numbers and completeness for the real order.
• The same full semantics is metatheoretically heavy: second-order truth depends more directly on set-theoretic background assumptions, and there is no effective complete proof system for full second-order validity analogous to first-order completeness.
• General or Henkin models restrict second-order variables to a specified collection of relations and functions. This recovers a smoother proof theory, including Henkin-style completeness, but loses the full-semantics categoricity phenomenon.
• Comprehension axioms supply relations defined by formulas; unrestricted comprehension is impredicative because the defining formula may quantify over relations in the same range.
• Monadic second-order logic has especially important computer-science fragments: MSO theories of successor structures and infinite binary trees are decidable via automata, and finite-model theory connects existential second-order definability with NP.
• Higher-order logic moves beyond relation and function variables over individuals to variables over objects of lower types; type theory is the systematic typed form of this progression.

Methods / Formalism

• A typical second-order induction axiom for natural numbers is:

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

• Full second-order semantics interprets an n-ary relation variable X as a subset of M^n, and an n-ary function variable F as a function M^n -> M.
• A representative 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)).$$

• General models replace unrestricted quantification over all subsets/functions with quantification over a supplied collection G of admissible relations and functions.
• See Full and Henkin Second-Order Semantics for the reusable full-vs-general-model clauses and their proof-theoretic implications.

Evidence / Experiments

• This is an encyclopedia survey, not a new theorem paper or empirical study.
• The entry synthesizes classical results from model theory, proof theory, finite model theory, and descriptive complexity.
• The current ingest reviewed the full clipped text and checked the SEP citation metadata for the archived Winter 2024 version.

Connections

• Seeds Second-Order Logic as the general concept page for property/relation/function quantification.
• Seeds Higher-Order Logic for the typed extension beyond second-order relation variables.
• Adds Full and Henkin Second-Order Semantics as the formal annex for the semantic fork between full and general models.
• Connects to Automata-Theoretic Logic and MSO Automata Correspondence through monadic second-order definability over words and trees.
• Connects to Temporal Logic because many temporal-logic decision procedures sit near MSO, automata translations, or tree-automata constructions.
• Connects to Formal Methods as background for specification languages, proof assistants, mechanized reasoning, and verification logics.

Open Questions

• Which source should become the wiki’s canonical technical reference for dependent type theory and Curry-Howard?
• Should Second-Order Logic later split off a dedicated page for descriptive complexity and Fagin’s theorem?
• When should wiki notes treat higher-order logic as a mathematical foundation, and when as proof-assistant implementation background?

Citation

Vaananen, Jouko. 2024. “Second-order and Higher-order Logic.” In The Stanford Encyclopedia of Philosophy, Winter 2024 edition, edited by Edward N. Zalta and Uri Nodelman. Metaphysics Research Lab, Stanford University. Stable archive: https://plato.stanford.edu/archives/win2024/entries/logic-higher-order/.