Is this theorem equivalent to "existential instantiation" rule?

Question

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?

Answer 1

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 :

• Assume $\Gamma$ and $\exists x \varphi$;

• by Existential instantiation we have :

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

Answer 2

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.