Henkin construction
= Henkin construction
{c}
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>.