Henkin Semantics

Origin. Henkin introduced general models for higher-order logic (1950). Alternative to standard semantics. Function spaces need not be full. Completeness theorem holds (unlike standard semantics). Foundation for much of higher-order logic.

Models. General vs standard models. Standard: function types are full function spaces. Henkin: function types can be proper subsets. Standard semantics: incomplete (Gödel). Henkin semantics: complete, axiomatizable. Trade-off: weaker categorical properties.

Formalism.

Standard model: D_τ→σ = D_σ^{D_τ} (all functions from D_τ to D_σ) Full: every possible function included.

Henkin model: D_τ→σ ⊆ D_σ^{D_τ} (subset of functions) General: only "definable" or chosen functions.

Closure conditions: Application: if f ∈ D_τ→σ and a ∈ D_τ, then f(a) ∈ D_σ. Abstraction: λ-definable functions must be in domain.

Completeness: Henkin semantics: HOL is complete. Standard semantics: HOL is incomplete.

Comprehension: ∃f.∀x. f(x) = t valid in standard, may fail in general. General models: only certain f exist.

Categoricity: Standard: categorical for arithmetic (unique up to iso). General: multiple non-isomorphic models.

Applications: Henkin models for type theory. Proof assistants (Isabelle/HOL) use Henkin-style.

Symbols.

Symbol	Unicode	Name	Meaning
λ	U+03BB	Lambda	Abstraction; the λ-definable functions the frame must contain
σ	U+03C3	Sigma	A type, the codomain in τ→σ
τ	U+03C4	Tau	A type, the domain in τ→σ
→	U+2192	Rightwards arrow	The function type constructor
∀	U+2200	For all	Universal quantifier
∃	U+2203	There exists	Existential quantifier, as in comprehension
∈	U+2208	Element of	Membership in a type domain
⊆	U+2286	Subset of or equal to	D_τ→σ ⊆ D_σ^{D_τ}: the domain need not be full
⊨	U+22A8	Satisfaction	Truth in a model
D_τ	—	Type domain	The set of objects of type τ
τ→σ	—	Function type	The type of functions from τ to σ
D_σ^{D_τ}	—	Full function space	Every function from D_τ to D_σ
f, a	—	Function and argument	The elements in the application condition
x, t	—	Variable and term	In the comprehension instance ∃f.∀x. f(x) = t
HOL	—	Higher-order logic	The logic these models interpret
frame	—	Type frame	The family of domains before closure conditions
general model	—	General model	A frame in which every term denotes
standard model	—	Standard model	A general model whose function domains are full

Metatheory. Under general models higher-order logic is a notational variant of many-sorted first-order logic: the domains are ordinary sets, application is a relation, and comprehension becomes a schema of axioms. Everything follows from that. Henkin (1950) proved the standard axiomatization of Church's simple theory of types complete for general models, and compactness and both Löwenheim–Skolem theorems transfer for the same reason, so the Henkin-valid sentences are recursively enumerable while the standard-valid ones are not. Andrews (1972) corrected the definition, requiring explicitly that every well-formed term have a denotation — closure under application does not deliver it. The cost is categoricity. Dedekind's second-order axioms for arithmetic and the second-order theory of the complete ordered field are categorical only under standard semantics; with general models they acquire non-isomorphic models exactly as their first-order counterparts do. The standard models are recoverable as those general models whose function domains are the full function spaces.

Applies to. Higher-order logic foundations. Proof assistants (HOL family). Type theory. λ-calculus semantics. Formal verification.

Limitations. General models gain completeness by giving up expressive power. Second-order quantifiers no longer range over all subsets, so the categorical characterizations that motivate second-order logic disappear: compactness holds under Henkin semantics, and therefore finiteness, well-foundedness, and the standard model of arithmetic cannot be pinned down up to isomorphism any better than in first-order logic. Sentences valid on standard models can fail on general ones — comprehension is a schema, and only its instances are guaranteed. Which frames count as general models is not fixed by the syntax: the closure conditions must be stipulated, and Andrews showed that a natural-looking definition is too weak. And the completeness result does not settle the philosophical question it is often enlisted for: Quine's objection that second-order logic is set theory in disguise targets standard semantics, which general models abandon rather than answer.