Prove $\vdash\forall x(\alpha\to\beta)\to(\exists x\alpha\to\exists x\beta)$

Question

I want to show that:

$\vdash\forall x(\alpha\to\beta)\to(\exists x\alpha\to\exists x\beta)$

I started my deduction as follows:

1. $\vdash\forall x(\alpha\to\beta)\to(\forall x\alpha\to\forall x\beta)$ ---------------------------------- Axiom $3$
2. $\vdash\forall x\alpha\to\alpha$ --------------------------------------------------------- Axiom $2$
3. $\vdash\forall x\neg\alpha\to\neg\alpha$ ----------------------------------------------------- Axiom $2$
4. $\vdash(\forall x\alpha\to\alpha)\to\big((\forall x\neg\alpha\to\neg\alpha)\to(\forall x\alpha\to\neg\forall x\neg\alpha)\big)$ ------ Axiom $1$
5. $\vdash(\forall x\neg\alpha\to\neg\alpha)\to(\forall x\alpha\to\neg\forall x\neg\alpha)$ -------------------------- Modus Ponens $2,4$
6. $\vdash\forall x\alpha\to\neg\forall x\neg\alpha$ -------------------------------------------------- Modus Ponens $3,5$
7. $\vdash\forall x\alpha\to\exists x\alpha$ ------------------------------------------------------ Definition $\exists$

What is the shortest way to complete this deduction? Having shown that $\vdash\forall x\alpha\to\exists x\alpha$, how do I formally explain that $\vdash\forall x\beta\to\exists x\beta$ ? When I have these two statements, can I apply Rule T to $(1)$ to yield the desired proposition?

Answer 1

You have to note that in Enderton's system $\exists$ is not primitive; thus, there are no rules for "managing" it.

We have use contraposition :

1) $∀x(α→β)$ --- assumed

2) $α→β$ --- from 1) and Ax.2 by mp

3) $\lnot \beta \to \lnot \alpha$ --- from 2) and Rule T

4) $∀x(\lnot \beta \to \lnot \alpha)$ --- from 3) and Gen Th

5) $∀x\lnot \beta \to ∀x\lnot \alpha$ --- from 4) and Ax.3 by mp

6) $\lnot ∀x\lnot \alpha \to \lnot ∀x\lnot \beta$ --- from 5) "contraposing" again (i.e. by Rule T)

7) $\exists x \alpha \to \exists x \beta$ --- abbreviation.

Thus, from 1) and 7) we conclude by Deduction Th with :

$\vdash ∀x(α→β) → (∃xα→∃xβ)$.