Is this theorem equivalent to “existential instantiation” rule?

In Enderton's, There is a theorem called "existential instantiation", it says:

Assume that the constant symbol $c$ does not occur in $\alpha ,\beta , \Gamma$ and that: $$\Gamma\cup\{\alpha^x_c\}\vdash\beta$$ Then $$\Gamma\cup\{\exists\alpha\}\vdash\beta$$

I've googled the name of the theorem but found that on Wikipedia here for example, It says something else namely, Given $\exists x\alpha$ we can infer $\alpha^x_c$ for some contant symbol $c$ that has not been used before in the deduction. It seems that what wikipedia states is the converse of the EL theorems in Enderton's and I don't see how both forms coincede.

Could anyone clarify for me how they state the same fact?

It is the existential elimination rule of Natural Deduction :

from $\Gamma, \varphi(y/x) \vdash \psi$, infer $\Gamma, \exists x \varphi \vdash \psi$, provided that $y$ is not free in $\psi$, or in any assumption in $\Gamma$.

The other rule of Natural Deduction for $\exists$ is the existential introduction rule :

from $\varphi(t)$, infer $\exists x \varphi(x)$

which in Enderton's system correspons to : $\vdash \alpha^x_t \rightarrow \exists \alpha$, that can be easily derived from Ax.2 : $\forall x \alpha \rightarrow \alpha^x_t$.

In order to understand Enderton's (apparent) "idiosyncratic" approach, we can see the very simple proof of Coroll.24H (Rule EI), page 124 :

Assume that the constant symbol $c$ does not occur in $\varphi, \psi$ or $\Gamma$, and that $\Gamma, \varphi^x_c \vdash \psi$.

By contraposition we have $\Gamma, \lnot \psi \vdash \lnot \varphi^x_c$ and by [previous result] we obtain : $\Gamma, \lnot \psi \vdash \forall \lnot \varphi^x_c$.

Applying contraposition again, we have the desired result.

"Informally", we can rephrase Enderton's proof as follows :

$\exists x \varphi \vdash \varphi^x_c$, where $c$ is an arbitrary constant symbol which does not occur in $\varphi, \psi$ or $\Gamma$.

By hypotheses :

• $\Gamma, \varphi^x_c \vdash \psi$;

thus, we can conclude with :

$\Gamma, \exists x \varphi \vdash \psi$.

Why not ? The issue is that the rule :

from $\exists x \varphi$, infer $\varphi^x_c$, for a new constant $c$

is not part of Enderton's Deductive Calculus [see page 109-on].

Why so ? Because, without some "tricky" provisos this rule is not sound in Enderton's calculus.

Assume that we can add this rule to the system; then we can "manufacture" this simple derivation :

1) $\exists x \varphi(x)$ --- assumed

2) $\varphi^x_c$ --- from 1), with a new constant $c$ not occurring in it.

Thus, we have the derivation : $\exists x \varphi(x) \vdash \varphi^x_c$.

Then we apply to it :

Coroll.24G [page 124] : Assume that $\Gamma \vdash \varphi^x_c$, where the constant symbol $c$ does not occur in $\Gamma$ or in $\varphi$. Then $\Gamma \vdash \forall x \varphi$, and there is a deduction of $\forall x \varphi$ from $\Gamma$ in which $c$ does not occur

with $\Gamma = \{ \exists x \varphi(x) \}$, and we have a new derivation :

$\exists x \varphi(x) \vdash \forall x \varphi$.

Finally apply the Deduction Th to get :

$\vdash \exists x \varphi(x) \rightarrow \forall x \varphi$.

But this formula is clearly invalid; consider its arithmetical instance : $\exists x(x \ne 0) \rightarrow \forall x(x \ne 0)$.

• Where is the elimination of the quantifier in the existential elimination rule? Also, In enderton's: $x$ must not occur in neither $\phi,\psi$ nor in any formula in $\Gamma$ but you require different condition. Another thing: it seems that the rule wiki talks about is existential introduction not elemination. – Fawzy Hegab Feb 1 '15 at 4:43
• @MathsLover - What Wiki call Existential instantiation is $\exists$-elimination; $\exists$-introduction corresponds to Existential generalization. – Mauro ALLEGRANZA Feb 1 '15 at 22:02
• Ok but you didn't get me, I wonder: If both the rule of quantifier elimination in natural deduction (As stated in wikipedia) and quantifier instantiation in Enderton's, capture the same intuitive idea, I don't see how both do capture the "same" idea. The statement stated in wiki seems more intuitive for me than the theorem in Enderton's so my essential question: How do we know that both are the same? notice that formulation of both statements are apparently different – Fawzy Hegab Feb 2 '15 at 3:32
• By "both formulations", I mean this formulation :en.wikipedia.org/wiki/Existential_instantiation , and the one given in Enderton's as stated in the question. – Fawzy Hegab Feb 2 '15 at 3:34
• @MathsLover- as you can see in Rules of inference : Existential Instantiation (or Existential Elimination), there are different way of formalizing the rules for $\exists$. – Mauro ALLEGRANZA Feb 2 '15 at 7:25

If you can infer $A$ from $B$, and you have $\Gamma \cup \{A\} \vdash \beta$, then you can conclude that $\Gamma \cup \{B\} \vdash \beta$. (The left-side of a turnstile is like the left-hand side of an implication: strengthening an assumption preserves validity.) Hence there is no conflict between Enderton's rule that operates on an assumption and the rule you found in the Wikipedia that operates on a conclusion.