Prove $(\forall x\ Q(x))\to P ⊢ \exists x (Q(x)\to P)$ using Natural Deduction

Question

I have stumbled upon this predicate logic sequent which I have trouble proving using natural deduction:

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

I started with ∀xQ(x) → P as the premise. I wanted to start using universal elimination but since the ∀x doesn't cover Q(x) → P completely, I refrained from doing so. I had to assume ∀xQ(x) but when I did, I couldn't reach ∃x(Q(x) → P) out of the assumption's scope.

I have also tried proof by contradiction but I couldn't progress. I tried to prove p → q ⊢ (¬p V q) with natural deduction to be able to incorporate it into the solution, but I couldn't prove it either.

So, I think I am completely stuck this one. Could you help me prove this (or tell me if this cannot be proved by natural deduction for any reason)?

If it helps, I am using the inference rules listed under https://en.wikipedia.org/wiki/List_of_rules_of_inference

Answer 1

Hint: you will need to use the law of the excluded middle (LEM) in whatever form it is presented in your system of natural deduction. By LEM, it suffices to consider two cases: (i) when $P$ is true and (2) when $P$ is false. In case (i) any implication of the form $A \to P$ is true and hence so is $\exists x(A \to P)$ for any formula $A$. In case (ii), we must have that $\forall xQ(x)$ is false, given that $\forall xQ(x) \to P$, so $\exists x \lnot Q(x)$ and an $x$ that witnesses that will also witness $\exists x (Q(x) \to P)$. I leave it to you to translate this into the system of natural deduction you are using.

Answer 2

Here's a skeleton of a proof by reduction to absurdity. Prove that it is absurd to assume that such a conditional does not exist.

$$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{(\forall x~Qx)\to P}{\fitch{\lnot\exists x~(Qx\to P)}{\fitch{\boxed a}{~~\vdots\\Qa}\\\forall x~Qx\\P\\\exists x~P\\\fitch{\boxed c~P}{~~\vdots\\\bot}\\\bot}\\\lnot\lnot\exists x~(Qx\to P)\\\exists x~(Qx\to P)}$$