Full and Henkin Second-Order Semantics

Context

Second-Order Logic gets much of its mathematical strength from quantifying over properties, relations, and functions. Vaananen2024 - Second-Order and Higher-Order Logic emphasizes that the key distinction is semantic: full models interpret those quantifiers over all subsets/functions of the domain, while general or Henkin models restrict them to a chosen collection.

Formal Statement

Let M be the domain of a first-order structure. In full second-order semantics, an n-ary relation variable X ranges over all subsets of M^n, and an n-ary function variable F ranges over all functions M^n -> M.

The existential clauses are:

$$M{\models }_s\exists X\varphi ⟺M{\models }_{s(P/X)}\varphi \text{ for some }P\subseteq M^n.$$ $$M{\models }_s\exists F\varphi ⟺M{\models }_{s(f/F)}\varphi \text{ for some }f:M^n\to M.$$

A general model is a pair (M,G), where G is a collection of admissible relations and functions over M. The corresponding clauses become:

$$(M,G){\models }_s\exists X\varphi ⟺(M,G){\models }_{s(P/X)}\varphi \text{ for some }P\in G.$$ $$(M,G){\models }_s\exists F\varphi ⟺(M,G){\models }_{s(f/F)}\varphi \text{ for some }f\in G.$$

A Henkin model is a general model satisfying the second-order proof-system axioms, including comprehension and relevant choice principles.

Derivation / Construction

Full semantics validates the intended reading of second-order induction:

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

where X ranges over every subset of the natural-number domain. Under that reading, second-order axioms can characterize structures such as the natural numbers or ordered real field up to isomorphism.

The proof-theoretic pressure comes from the comprehension schema:

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

If phi may itself quantify over relation variables in the same range, the schema is impredicative. General models handle this by making the available relation/function range explicit as G. Henkin models are the general models rich enough to satisfy the axioms, but not necessarily full.

Implications

• Full semantics supports categoricity-style mathematical claims, but full second-order validity does not have an effective complete proof system analogous to first-order logic.
• Henkin semantics supports a completeness theorem and behaves more like many-sorted first-order logic, but it weakens full-categoricity intuitions.
• A proof or verification note should say which semantic reading it relies on when categoricity, compactness, or completeness matters.
• Automata-theoretic uses of monadic second-order logic usually work inside restricted structures where decidability or translation results, rather than unrestricted full semantics, do the practical work.

Links

• Second-Order Logic
• Higher-Order Logic
• Automata-Theoretic Logic
• Vaananen2024 - Second-Order and Higher-Order Logic