Derive $\forall x (P(x) \to Q(x)) \to (\exists x P(x) \to \exists x Q(x))$

Question

I tried to derive $\forall x (P(x) \to Q(x)) \to (\exists x P(x) \to \exists x Q(x))$ using deduction lemma but without Godel's Theorem, but I stucked.

My attempt. Let's use deduction lemma and add $\forall x (P(x) \to Q(x))$ to our axioms. Now we have to derive $\exists x P(x) \to \exists x Q(x)$. Okay, let's use deduction lemma one more time and now add $\exists x P(x)$ to our axioms. Finally we have to prove $\vdash \exists x Q(x)$. From $\forall x (P(x) \to Q(x))$ we can obtain $\vdash P(x) \to Q(x)$, but it seems useless. From second formula using modus ponens one can obtain $\vdash \exists x Q(x) \to \exists x P(x)$ but it also seems extremely useless. Unfortunately, Bernays rules are not applicable to $\forall x (P(x) \to Q(x))$. For sure I have to use some tautology but I'm confused.

Edit. I can use:

1. Special cases of tautologies.
2. $A(t) \to \exists u A(u)$.
3. $\forall u A(u) \to A(t)$.
4. Modus ponens.
5. Bernays rule 1.
6. Bernays rule 2.
7. Deduction lemma.

Answer 1

Assuming the equivalence between $\forall$ and $\lnot \exists \lnot$, here is a proof sketch...

1) $∀x(P(x)→Q(x))$ --- premise

2) $P(x)→Q(x)$ --- from 1) by quantifier axiom : $∀u A(u) → A(t)$ and modus ponens

3) $\lnot Q(x) → \lnot P(x)$ --- from 2) by tautological implication

4) $\forall x \lnot Q(x)$ --- assumed [a]

5) $\lnot Q(x)$ --- from 4) by quantifier axiom

6) $\lnot P(x)$ --- from 3) and 5) by mp

7) $\forall x \lnot Q(x) \to \lnot P(x)$ --- from 4) and 6) by Deduction Theorem, discharging assumption [a]

8) $\forall x \lnot Q(x) \to \forall x \lnot P(x)$ --- using Bernays' rule : if $C \to A(x)$, then $C \to \forall x A(x)$, provided that $x$ is not free in $C$

9) $\lnot \forall x \lnot P(x) \to \lnot \forall x \lnot Q(x)$ --- from 8) by tautological implication

10) $\exists x P(x) \to \exists x Q(x)$ --- from 9) by equivalence between quantifiers.

---

We can avoid the equivalence between quantifiers ...

To do this, we need a "derived rule", the so-called $\exists$-elimination rule, easily proved with Bernays' rule : if $\Gamma, A(x) \vdash C$, then $\Gamma, \exists x A(x) \vdash C$, with $x$ not free in $C$ nor in $\Gamma$.

1)-2) as above

3) $\exists xP(x)$ --- assumed [a]

4) $P(x)$ --- assumed [b]

5) $Q(x)$ --- from 2) and 4) by mp

6) $\vdash Q(x) \to [(\lnot R \lor R) \to Q(x)]$ --- tautology : $A \to (B \to A)$

7) $(\lnot R \lor R) \to Q(x)$ --- from 5) and 6) by mp

8) $(\lnot R \lor R) \to \forall x \ Q(x)$ --- by Bernays' rule

9) $\vdash \lnot R \lor R$ --- tautology

10) $\forall x \ Q(x)$ --- from 9) and 8) by mp

From 4)-10) we have : $P(x) \vdash \forall x \ Q(x)$; we apply the $\exists$-elimiantion rule ($x$ is not free in $\forall x \ Q(x)$, nor in the premise 1)) to derive :

11) $\exists x \ P(x) \vdash \forall x \ Q(x)$

12) $\exists x \ P(x) \vdash \exists x \ Q(x)$ --- from 11) by the quantifier axioms and mp

13) $\exists x \ P(x) \to \exists x \ Q(x)$ --- from 12) by Deduction Th.