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.
A full set of first-order sentences has existential witnesses among names in its own first-order language: if it proves an existential sentence, it proves some closed-term instance of the matrix. For a deductively closed set this may be stated by membership of the first-order sentences. In a function-free first-order language the witness is a constant symbol. A first-order consistent complete full first-order theory has a canonical term model.
A Henkin witness axiom names a witness to an existential sentence using a fresh constant symbol. Freshness is part of the consistency-preservation argument in the Henkin construction.
Articles by others on the same topic
There are currently no matching articles.