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)$.

  • $\begingroup$ 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. $\endgroup$ – Fawzy Hegab Feb 1 '15 at 4:43
  • $\begingroup$ @MathsLover - What Wiki call Existential instantiation is $\exists$-elimination; $\exists$-introduction corresponds to Existential generalization. $\endgroup$ – Mauro ALLEGRANZA Feb 1 '15 at 22:02
  • $\begingroup$ 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 $\endgroup$ – Fawzy Hegab Feb 2 '15 at 3:32
  • $\begingroup$ 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. $\endgroup$ – Fawzy Hegab Feb 2 '15 at 3:34
  • $\begingroup$ @MathsLover- as you can see in Rules of inference : Existential Instantiation (or Existential Elimination), there are different way of formalizing the rules for $\exists$. $\endgroup$ – 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.