next up previous contents
Next: Examples Up: Quantifier reasoning Previous: Existential quantifier introduction   Contents

Existential quantifier elimination

Oftentimes when we know a statement of the form $\exists \; x \, . \, F$, we reason as follows: ``We know that there is something for which $F$ holds. Let $w$ be a name for that something, so that $F$ holds for $w$. Then $\cdots$'' where $\cdots$ is a derivation of some conclusion $G$, presumably with the help of the premise that $F$ holds for $w$, i.e., the premise $F[x \mapsto w]$. It is customary to refer to $w$ as a witness, and to the formula $F[x \mapsto w]$ as the witness premise. No special assumptions about the witness $w$ must be made; It must serve only as a ``dummy''--any other name should do just as well. In particular, the witness should not occur in the final conclusion $G$. This form of reasoning is captured in NDL with deductions of the form

\begin{displaymath}\mbox{\tt pick-witness } x \,\mbox{\tt for (exists x} \; F\mbox{\tt )} \;\; D\end{displaymath}

Their semantics are as follows:
$\;\;$ $\mbox{$\beta$}\cup \{F[x\mapsto v]\} \mbox{$\:\vdash\:$}\{x \mapsto v\}D \mbox{$\:\longrightarrow\;$}G$$\;$  
  $\;\:$
$\;\;$
$\mbox{$\beta$}\mbox{$\:\vdash\:$}\mbox{\tt pick-witness } w \mbox{\tt for (exists $x$} \;\: F\mbox{\tt )} \;\;
D \mbox{$\:\longrightarrow\;$}G$
provided $v$ does not occur in $\beta$, in $D$, or in $G$.
$\;$
 
Here $v$ is a freshly generated variable, which helps to ensure that the witness is used only as a dummy.
next up previous contents
Next: Examples Up: Quantifier reasoning Previous: Existential quantifier introduction   Contents
2004-08-04