View source for Henkin construction

The method of constants was introduced by L. Henkin in 1949 [[#References|[a1]]] to establish the strong completeness of first-order logic (cf. [[Completeness (in logic)|Completeness (in logic)]]). Whilst this method originally involved the deductive apparatus of first-order logic, it can be modified so as to employ only model-theoretic ideas (cf. [[Model (in logic)|Model (in logic)]]; [[Model theory|Model theory]]).

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h1101501.png" /> be a first-order logical language with equality, and consider a set of sentences in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h1101502.png" /> which is finitely satisfiable in the sense that each of its finite subsets has a model. Since the collection of finitely satisfiable sets is closed under unions of chains, each such set can be extended to one which is maximal in the sense that it is finitely satisfiable and contains every sentence in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h1101503.png" /> or its negation. When <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h1101504.png" /> contains constant terms, each maximal set in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h1101505.png" /> induces an [[Equivalence|equivalence]] relation on the set of constant terms: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h1101506.png" /> is in this relation provided that the equation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h1101507.png" /> is a member of the maximal set. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h1101508.png" /> denote the equivalence class of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h1101509.png" />. An [[Interpretation|interpretation]] for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015010.png" /> can be constructed on the partition induced by this relation. On this interpretation, each individual constant in the non-logical vocabulary of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015011.png" /> denotes its equivalence class; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015012.png" /> is in the extension of the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015013.png" />-ary predicate <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015014.png" /> if and only if the sentence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015015.png" /> is a member of the maximal set; and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015016.png" /> is in the extension of the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015017.png" />-ary functional constant <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015018.png" /> if and only if the equation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015019.png" /> is a member of the maximal set. This interpretation is a model of the maximal set if the set is term-complete in the sense that it contains an instance of each existential sentence it contains. This interpretation is called a Henkin model for the maximal and term-complete set.

Not every first-order language contains constant terms. And even when <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015020.png" /> contains constant terms, there are finitely satisfiable sets in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015021.png" /> which cannot be extended to maximal and term-complete sets in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015022.png" />. In such cases the Henkin construction proceeds by adding new constants to the non-logical vocabulary of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015023.png" /> in such a way that the finitely satisfiable set in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015024.png" /> can be extended to a maximal and term-complete set in the extended language.

H.J. Keisler [[#References|[a2]]] modified the Henkin construction at the point where the new constants are introduced. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015025.png" /> denote the collection of finite subsets of a finitely satisfiable set. For each member of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015026.png" />, choose a model of that set. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015027.png" /> is the family (indexed by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015028.png" />) of such models. Expand the non-logical vocabulary of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015029.png" /> by adding the members of the direct product of the domains of the members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015030.png" /> as individual constants. Members of this direct product are functions on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015031.png" /> whose value at each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015032.png" /> is a member of the domain of the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015033.png" />th member of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015034.png" />. The <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015035.png" />th member of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015036.png" /> is expanded to interpretations of the extended language by having each function in the direct product denote its value at <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015037.png" />. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015038.png" /> denote the resulting family of interpretations. The theory of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015039.png" /> is the set of all sentences in the extended language true on all members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015040.png" />. The union of the theory of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015041.png" /> and the finitely satisfiable set from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015042.png" /> is itself finitely satisfiable, and any maximal extension of this union is term complete. The Henkin model for such a maximal extension is called a Henkin–Keisler model.

Generalizing the above, let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015043.png" /> be any non-empty set and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015044.png" /> be a family of interpretations for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015045.png" /> indexed by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015046.png" />. As above, expand the non-logical vocabulary of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015047.png" /> by adding the direct product of the domains of the members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015048.png" /> as individual constants, expand the members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015049.png" /> to interpretations of the extended language as above, and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015050.png" /> denote the resulting family of interpretations. The theory of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015051.png" /> is finitely satisfiable and any maximal extension of this set is term complete.

Henkin–Keisler models can be seen as both a specialization of the Henkin construction and as an alternative to the ultraproduct construction (cf. also [[Ultrafilter|Ultrafilter]]). There is a natural correspondence between maximal extensions of the theory of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015052.png" /> and ultrafilters (cf. [[Ultrafilter|Ultrafilter]]) on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015053.png" />. Associate with each sentence in the expanded language the set of indices (from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015054.png" />) of those members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015055.png" /> on which the sentence is true. Given an ultrafilter on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015056.png" />, consider the set of sentences in the extended language whose associated set of indices is a member of the ultrafilter. This set is a maximal extension of the theory of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015057.png" />. Further, if all members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015058.png" /> are non-trivial in the sense that their domains contain at least two objects, then given any maximal extension of the theory of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015059.png" />, the collection of sets of indices associated with the members of the maximal extension is an ultrafilter on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015060.png" />. Finally, the Henkin–Keisler model of any maximal extension of the theory of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015061.png" />, when restricted to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015062.png" />, is isomorphic to the ultraproduct of the members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/h/h110/h110150/h11015063.png" /> over the corresponding ultrafilter.

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  L. Henkin,   "The completeness of the first-order functional calculus"  ''J. Symb. Logic'' , '''14'''  (1949)  pp. 159–166</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  H.J. Keisler,   "A survey of ultraproducts, logic"  Y. Bar-Hillel (ed.) , ''Logic, Methodology and Philosophy of Science'' , North-Holland  (1965)  pp. 112–126</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  G. Weaver,   "Henkin–Keisler models" , Kluwer Acad. Publ.  (1997)</TD></TR></table>