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.
New to topics? Read the docs here!