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 $t$ has a certain property $F$, then we should be able to conclude that there exists something that has the property $F$. This is called existential quantifier introduction. In NDL, it is performed with proofs of the form

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

whose semantics are as follows:

\begin{displaymath}\mbox{$\beta$}\cup \{F[x \mapsto t]\} \mbox{$\:\vdash\:$}
\m...
...om $t$} \mbox{$\:\longrightarrow\;$}\mbox{\tt (exists $x$ $F$)}\end{displaymath}

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

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

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

2004-08-04