How to derive $\exists$ Elimination rule in Enderton's system

Question

I'm trying to derive the following rule :

from $α→β$, infer $(∃x)α→β$, provided that $x$ is not free in $β$

in the system of Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001).

The axioms are [see page 112] :

The logical axioms are all generalizations of wffs of the following forms, where $x$ and $у$ are variables and $\alpha$ and $\beta$ are wffs:

1. Tautologies;

2. $\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$ in $\alpha$;

3. $\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$;

4. $\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$.

If the language includes equality, the usual axiom for it are added.

Modus ponens is the sole rule of inference.

---

What we can prove in Enderton's system is the following meta-theorem :

if $\Gamma \vdash \alpha \rightarrow \beta$, and $x$ is not free in $\beta$ nor in any formula in $\Gamma$, then : $\Gamma \vdash \exists x \alpha \rightarrow \beta$.

Proof :

We have to start from :

(1) $\Gamma \vdash \alpha \rightarrow \beta$

(2) $\Gamma \vdash \lnot \beta \rightarrow \lnot \alpha$ --- from (1) and Taut, by mp

(3) $\lnot \beta$ --- assumed

(4) $\Gamma, \lnot \beta \vdash \lnot \alpha$.

Now, due to the proviso, we can apply the Gen Th to have :

(5) $\Gamma, \lnot \beta \vdash \forall x \lnot \alpha$

(6) $\Gamma \vdash \lnot \beta \rightarrow \forall x \lnot \alpha$ --- from (3) and (5), by Deduction Theorem

(7) $\Gamma \vdash \lnot \forall x \lnot \alpha \rightarrow \beta$ --- from (6) and Taut, by mp

(8) $\Gamma \vdash \exists x \alpha \rightarrow \beta$ --- abbreviation.

From this theorem, under the same proviso, with $\Gamma = \emptyset$ we have :

(A) if $\vdash \alpha \rightarrow \beta$, then $\vdash \exists x \alpha \rightarrow \beta$.

---

Note : these rules are not stated in Enderton's book, but we can easily derive the last one from the theorem in Example (Q3B) [page 122] :

$\vdash (\exists x \alpha \rightarrow \beta) \leftrightarrow \forall x(\alpha \rightarrow \beta)$, provided that $x$ does not occur free in $\beta$.

Proof :

(1) $\vdash \alpha \rightarrow \beta$

(2) $\vdash \forall x(\alpha \rightarrow \beta)$ --- by Generalization Theorem [page 117] : if $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$, with $\Gamma = \emptyset$.

(3) $\vdash \exists x \alpha \rightarrow \beta$ --- by (Q3B).

In the same way, from the theorem of Example (Q2A) [page 121] :

$\vdash (\alpha \rightarrow \forall x \beta) \leftrightarrow \forall x(\alpha \rightarrow \beta)$, provided that $x$ does not occur free in $\alpha$,

we can prove the meta-theorem :

(B) if $\vdash \alpha \rightarrow \beta$, then $\vdash \alpha \rightarrow \forall x \beta$,

with the same proviso.

Of course, we can deduce it from the "more general" meta-theorem :

if $\Gamma \vdash \alpha \rightarrow \beta$, and $x$ is not free in $\alpha$ nor in any formula in $\Gamma$, then : $\Gamma \vdash \alpha \rightarrow \forall x \beta$

which can easily be proved as the other one.

The rules (A) and (B) are the Rules for the Universal and Existential Quantifiers used by David Hilbert & Wilhelm Ackermann, Principles of Mathematical Logic (2nd ed - 1937; see english translation, page 70) and due to Paul Bernays (see footnote); they are used also by S.C.Kleene in his textbooks.

Answer 1

The rule

from $α→β$, infer $(∃x)α→β$, provided that $x$ is not free in $β$,

without "constraint" on the assumption $\alpha \rightarrow \beta$, is not sound.

Let $\alpha := x = y$ and let $\beta := \forall x (x = y)$; the proviso that $x \notin FV(\beta)$ is satisfied.

If we apply the above rule, we get :

$\exists x (x = y) \rightarrow \forall x (x = y)$.

But this is not true in a domain with more than one element.

Thus, we need the assumption in the form : $\Gamma \vdash \alpha \rightarrow \beta$, whit proviso that $x$ is not free in $β$ nor in any formula in $\Gamma$.

If we try to use in the "unconstrained" form, we are using it with $\Gamma = \{ α→β \}$, and in this case it is nor more true that $x$ is not free in any formula in $\Gamma$.

Answer 2

I don't know if this works, and it's definitely not formal since I'm not listing the tautologies properly, but maybe it'll get you thinking.

assumption   (1) (α→β) 

hypothesis   (2) (∃x)α 

axiom 4      (3) [(α→β)→∀x(α→β)]

MP (1), (3)  (4) ∀x(α→β)

axiom 3      (5) [∀x(α→β)→(∀xα→∀xβ)]

MP (5), (4)  (6) (∀xα→∀xβ)

MP, Taut, (6) (7) (¬∀xβ→¬∀xα)  (the tautology is CCpqCNqNp in Polish notation)

MP, Taut, (7) (8) (¬¬∀xβ $\lor$ ¬∀xα) (the tautology is CCpqANpq)

MP, Taut, (8) (9)  (¬¬∀xβ $\lor$ ¬∀x¬¬α) (the tautology is CANNpqANNpNNq)

Def. of ∃     (10) (¬¬∀xβ $\lor$ ∃x¬α)

MP twice, Taut, 10, 2  (11) ¬¬∀xβ (the tautology is CANNpNqCqNNp)

MP Taut, 11 (12) ∀xβ (the tautology is CNNpp)

axiom 2     (13) ∀xα→α[x/t]

MP, 13, 12  (14) β

DT 2-14      (15) ((∃x)α→β)