= Henkin semantics
{c}
In <Henkin semantics>, a domain $D$ is accompanied by designated ranges $\mathcal H_k\subseteq\mathcal P(D^k)$ for <second-order relation variables> of each arity $k$. A formula $\exists R\,\varphi(R)$ searches only $\mathcal H_k$, and $\forall R\,\varphi(R)$ checks only $\mathcal H_k$. These ranges can be proper subcollections of the external <power set>. Keeping $D$ and its input relations fixed therefore need not fix the truth of a <second-order logic> sentence.
As a toy illustration of restricted quantification, take $D=\{a,b\}$ and unary range $\mathcal H_1=\{\varnothing,D\}$. The sentence
$$
\forall a\,\exists P\,\forall x\,(P(x)\leftrightarrow x=a)
$$
is true under <full semantics for second-order logic>, but false with this selected range, because neither singleton is available. Likewise, on the <complete graph> $K_3$, the unary range $\{\varnothing,D\}$ admits no witness for the <second-order encoding of three-colorability>, even though a usual <proper vertex coloring> exists. This toy range illustrates the truth definition only: it fails <second-order comprehension> for the formula $x=a$, and is not a model of a system requiring that comprehension instance.
Admissible <Henkin semantics> for a specified deductive system must satisfy its <axioms>, including its chosen <second-order comprehension> requirements or analogous closure conditions for predicate abstraction. Closure is relative to the permitted formulas and parameters, rather than a blanket property of every selected family. In particular, on a finite domain, allowing <logical equality>, individual parameters, all finite <logical disjunctions>, and comprehension for those formulas forces every finite-arity relation to be available: enumerate its <tuples> and disjoin the formulas naming them. Thus a proper restricted finite range cannot satisfy that entire scheme.
Treating each $\mathcal H_k$ as an additional sort, with an application relation between its members and $k$ individuals, translates this relational presentation into <first-order logic> with several sorts. Include <axioms> saying that predicates with the same members are equal, together with whatever <second-order comprehension> the system requires. This makes <Henkin semantics> useful for bringing <first-order logic> methods to reasoning about predicates; it does not license conclusions about all external relations.
Leon Henkin's https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/completeness-in-the-theory-of-types1/551D2896D3C6F197030D3D8EEA911F1E[Completeness in the Theory of Types, Journal of Symbolic Logic 15 (1950), pp. 81–91] develops general models and proves completeness for his typed deductive system. Its opening footnote 5 explicitly discusses closure under operations associated with formula formation. Henkin later described the discovery process in his https://www.cambridge.org/core/journals/bulletin-of-symbolic-logic/article/abs/discovery-of-my-completeness-proofs/D414E205C8FE0F4F1DCABA9EDAD72B36[1996 author retrospective, The Discovery of My Completeness Proofs]{ref}; that later account is a historical recollection, distinct from the original publication.
Back to article page
