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
D_τ	—	Domain	Type τ's domain
τ→σ	—	Function type	Functions τ to σ
λ	U+03BB	Lambda	Abstraction
∀	U+2200	Universal	For all
∃	U+2203	Existential	Exists
⊨	U+22A8	Satisfies	Models

Metatheory. Completeness: HOL complete for Henkin semantics. Compactness: holds for Henkin. Löwenheim-Skolem: holds for Henkin. Non-categoricity: Henkin models vary. Proof theory: matches general semantics.

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

Limitations. Weaker than standard semantics. Less categorical strength. Some intuitively valid formulas may fail. Philosophical status debated. Choosing "right" general model.