Definition:Witness Property

From ProofWiki
Jump to navigation Jump to search

Definition

Let $\LL$ be a language of predicate logic.

Let $\mathscr M$ be a formal semantics for $\LL$.

Let $\FF$ be a set of $\LL$-WFFs.


Suppose that, for every $\LL$-WFF of $1$ free variable $\map \phi x$, if:

$\FF \models_{\mathscr M} \exists x : \map \phi x$

then there exists some term $t$ containing no variables such that:

$\FF \models_{\mathscr M} \map \phi {x := t}$


Then, $\FF$ satisfies the witness property.


Sources