7.2.3 Existential elimination

Extracting some truth from a $\exists xPx$ is tricky, but it's done this way:


\begin{displaymath}\begin{fitch*}
\par
m & \exists x A \\
\par
n & \fh A\{a/x\}...
...
\par
\hline
\par
& B & E$\exists$\ m,n,p,a
\par
\end{fitch*} \end{displaymath}

So, if one of the $A$ implies $B$, then we know that $B$, since we know that one of the $A$ is true. No $a$ should appear in $B$ nor in any attainable hypothesis (sorry for the cryptical phrases, they are part of the theory).



Daniel Clemente Laboreo 2005-05-17