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

Universal quantifier elimination

If we know that something is true of everything, then we should be able to conclude that it is true of a particular individual $t$. This is called universal elimination because we go from $\forall \; x \, . \, F$ to $F[x\mapsto t]$, thereby removing the quantifier forall. In NDL this is performed by specialize, whose semantics are as follows:

\begin{displaymath}\mbox{$\beta$}\cup \{\mbox{\tt (forall x }\; F\mbox{\tt )}\} ...
...)} \mbox{\tt with } t \mbox{$\:\longrightarrow\;$}F[x\mapsto t]\end{displaymath}

It is an error if the universal quantification $\mbox{\tt (forall x }\; F\mbox{\tt )}$ is not in the assumption base. As an example, if $\beta$ contains (forall x male(father(x))), then

\begin{displaymath}\mbox{\tt specialize (forall x male(father(x))) with ann}\end{displaymath}

will produce the conclusion male(father(ann)).

2004-08-04