Definition:Witness Property

From ProofWiki
Jump to navigation Jump to search


An $\LL$-theory $T$ is said to have the witness property if for every $\LL$-formula $\map \phi v$ with one free variable, there is a constant symbol $c$ in $\LL$ such that:

$T \models \paren {\exists v \map \phi v} \to \map \phi c$

that is, $\paren {\exists v \map \phi v} \to \map \phi c$ is a semantic consequence of $T$.

That is, every existential statement satisfied by $T$ is witnessed by a constant.