First-order Logic Formalisation, Sentential Logic Formalisation

Question

I am not sure how to use the 'Existential Elimination' rule to prove the following derivation:

∀x(Px → Qa) ⊢ ∃xPx → Qa

I understand I need to eliminate the universal quantifier but I am unsure where to go from there. Would I combine existential elimination with a conditional proof in this instance?

Answer 1

You would.

$$\begin{array}{rcll}(\exists x)Px&\vdash&Pb&\text{(Existential Elimination, new } b)\\(\forall x)(Px\to Qa)&\vdash&Pb\to Qa&\text{(Universal Elimination.)}\\Pb\to Qa, Pb&\vdash&Qa&\text{(Modus Ponens).}\end{array}$$

Thus, $(\forall x)(Px\to Qa), (\exists x)Px\vdash Qa$.

Now, use conditional proof (Deduction Theorem) to claim that $(\forall x)(Px\to Qa)\vdash (\exists x)Px\to Qa$.