 Witness constant

A witness constant is a fresh constant symbol added to a first-order language so that an existential assertion has a named witness. In a Henkin construction one adds $\exists x\theta (x)\to \theta (c_{\theta })$, with $c_{\theta }$ absent from the previous language. Freshness preserves consistency. Repeating the construction for the successively enlarged languages supplies the witness property used in a term model.