Henkin construction

The method of constants was introduced by L. Henkin in 1949 [a1] to establish the strong completeness of first-order logic (cf. 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 theory).

Let be a first-order logical language with equality, and consider a set of sentences in 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 or its negation. When contains constant terms, each maximal set in induces an equivalence relation on the set of constant terms: is in this relation provided that the equation is a member of the maximal set. Let denote the equivalence class of . An interpretation for can be constructed on the partition induced by this relation. On this interpretation, each individual constant in the non-logical vocabulary of denotes its equivalence class; is in the extension of the -ary predicate if and only if the sentence is a member of the maximal set; and is in the extension of the -ary functional constant if and only if the equation 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 contains constant terms, there are finitely satisfiable sets in which cannot be extended to maximal and term-complete sets in . In such cases the Henkin construction proceeds by adding new constants to the non-logical vocabulary of in such a way that the finitely satisfiable set in can be extended to a maximal and term-complete set in the extended language.

H.J. Keisler [a2] modified the Henkin construction at the point where the new constants are introduced. Let denote the collection of finite subsets of a finitely satisfiable set. For each member of , choose a model of that set. is the family (indexed by ) of such models. Expand the non-logical vocabulary of by adding the members of the direct product of the domains of the members of as individual constants. Members of this direct product are functions on whose value at each is a member of the domain of the th member of . The th member of is expanded to interpretations of the extended language by having each function in the direct product denote its value at . Let denote the resulting family of interpretations. The theory of is the set of all sentences in the extended language true on all members of . The union of the theory of and the finitely satisfiable set from 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 be any non-empty set and let be a family of interpretations for indexed by . As above, expand the non-logical vocabulary of by adding the direct product of the domains of the members of as individual constants, expand the members of to interpretations of the extended language as above, and let denote the resulting family of interpretations. The theory of 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). There is a natural correspondence between maximal extensions of the theory of and ultrafilters (cf. Ultrafilter) on . Associate with each sentence in the expanded language the set of indices (from ) of those members of on which the sentence is true. Given an ultrafilter on , 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 . Further, if all members of are non-trivial in the sense that their domains contain at least two objects, then given any maximal extension of the theory of , the collection of sets of indices associated with the members of the maximal extension is an ultrafilter on . Finally, the Henkin–Keisler model of any maximal extension of the theory of , when restricted to , is isomorphic to the ultraproduct of the members of over the corresponding ultrafilter.

References

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