A Henkin construction enlarges a consistent first-order theory by fresh constants, decides sentences while preserving consistency, and supplies constant witnesses for existential sentences. Countably many additional dense requirements can be interleaved, as in the omitting types theorem. A complete consistent extension with witnesses has a term model.
For a complete consistent theory with the Henkin witness property, the term model has closed terms modulo provable equality as elements. Functions are evaluated by forming terms, and atomic relations hold exactly when the corresponding atomic sentences belong to the theory. Provable equality makes these interpretations well defined.
A sentence with closed-term parameters holds in a term model if and only if it belongs to the complete consistent theory defining that model. Prove this by structural induction: atoms are the definition, Boolean steps use completeness and consistency, and existential sentences use the Henkin witness property. Conversely any existential witness represented by a term gives the existential sentence by logical inference.
A theory in a language with constants has the Henkin witness property when every existential sentence belonging to it has an instance belonging to it for some constant . This property proves the existential step of the truth lemma for a Henkin term model.
Articles by others on the same topic
There are currently no matching articles.