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

Existential quantifier introduction

If we know that a particular object \bgroup\color{red}$t$\egroup has a certain property \bgroup\color{red}$F$\egroup, then we should be able to conclude that there exists something that has the property \bgroup\color{red}$F$\egroup. This is called existential quantifier introduction. In NDL, it is performed with proofs of the form

\begin{displaymath}\bgroup\color{red} \mbox{\tt ex-generalize (exists $x$ $F$) from $t$}\egroup\end{displaymath}

whose semantics are as follows:

\begin{displaymath}\bgroup\color{red}\mbox{$\beta$}\cup \{F[x \mapsto t]\} \mbox...
... \mbox{$\:\longrightarrow\;$}\mbox{\tt (exists $x$ $F$)}\egroup\end{displaymath}

For instance, assuming that the assumption base contains the atomic formula odd(3), the deduction

\begin{displaymath}\bgroup\color{red}
\mbox{\tt ex-generalize (exists x odd(x)) from 3}
\egroup\end{displaymath}

will produce the conclusion (exists x odd(x)).

2004-08-06