Henkin witness axiom (source code)

= Henkin witness axiom
{c}
{title2=$\exists x\theta(x)\to\theta(c_\theta)$}

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>.