= Witness constant
{title2=$\exists x\theta(x)\to\theta(c_\theta)$}
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 <consistent first-order theory>[consistency]. Repeating the construction for the successively enlarged languages supplies the witness property used in a <term model>.
Back to article page
