Derivation of null-quantified implication.

Question

I'm supposed to derive $\exists x(P \to Q(x))$ from $P \to \exists xQ(x)$ using only the basic introduction/elimination rules from used in Fitch. I've tried this by means of contradiction and universal introduction but I get stuck because I don't know how to deal with the null quantified $P$. There seems to be some trick that I'm supposed to apply which I can not figure out.

Any help would be greatly appreciated.

Allowed rules:

$\land$-introduction/-elimination

$\lor$-introduction/-elimination

$\neg$-introduction/-elimination

$\forall$-introduction/-elimination

$\exists$-introduction/-elimination

$\bot$-introduction/-elimination

$\to$-introduction/-elimination

$=$-introduction/-elimination

Answer 1

You were right to try to do a proof by contradiction. You can then try to prove the universal, but what you really want is just $P$ ... and that you can do by a proof by contradiction as well. And once you have $P$, it's easy. Here's the proof:

Answer 2

You have $P\to \exists xQ(x).$ Now assume $P.$ Eliminating $\to,$ you have $\exists xQ(x). $ Eliminating $\exists,$ you have $Q(c).$ By $\to$ introduction you have $P\to Q(c)$ and you discharge the assumption of $P.$ Then by $\exists$ introduction you have $\exists x(P\to Q(x)).$

Answer 3

You are trying to establish $P \to \exists x~Qx \vdash \exists x ~ (P \to Qx)$. It will help to first work on proving an almost equivalent but much easier claim:

$$B \to (C \lor T) \vdash (B \to C) \lor (B \to T)$$

The hangup here is the "knowing which one it is" issue. In constructive reasoning $A \lor B$ always means that you know which one of $A$ or $B$ holds. Consider the following conversation (the analogy is that $B$ is blueprints, $C$ is car, $T$ is truck) :

Alice asserts: "If I give Bob the blueprints in that desk, then Bob can build a car, or he can build a truck, and he'll know which one once he sees the blueprints."

Based on that, Bob responds with: "If Alice gives me the blueprints in that desk then I can build a car, or if she gives me the blueprints in the desk then I can build a truck: and I know which one it will be (before I even see the blueprints)".

Hopefully you'll say to Bob "How the heck will you know which before you see the blueprints?" If Bob answers "I always know whether blue prints are for a car or not, even before I see them, same for trucks" then (a) that is a pretty awesome useless skill and (b) his response now makes sense. So that means that what Bob is really saying is:

$$\begin{array} {rll} & B \to (C \lor T) \\ & (B \to C) \lor \lnot (B \to C) \\ & (B \to T) \lor \lnot (B \to T) \\ \hline \therefore & (B \to C) \lor (B \to T) \end{array}$$

Back to the original question, Bob's assumptions are the like saying that $P \to Qx$ is always decidable, that is $\forall x ~ (P \to Qx) \lor \lnot (P \to Qx)$. So to prove this LEM you probably want to approach the question like

$$(P \to Qt) \lor \lnot(P \to Qt),~ P \to \exists x ~Qx \vdash \exists x ~(P \to Qx)$$

(I'm trying to make it clear why $P \to Qx$ is the statement that has to be instantiated with LEM using the example of cars and trucks and blueprints, I hope it is clear enough).

So the proof follows using straightforward natural deduction now:

$$\begin{array} {rll} (1) & (P \to Qt) \lor \lnot(P \to Qt) & \text{Law of Excluded Middle} \\ (2) & P \to \exists x ~Qx & \text{Premise} \\ \\ (3) & \quad \quad P \to Qt & \text{Assumption (case 1)} \\ (4) & \quad \quad \exists x ~ (P \to Qx) & \text{From 4} \\ \\ (5) & \quad \quad \lnot (P \to Qt) & \text{Assumption (case 2)} \\ (6) & \quad \quad \quad \quad Qt & \text{Assumption} \\ (7) & \quad \quad \quad \quad \quad \quad P & \text{Assumption} \\ (8) & \quad \quad \quad \quad \quad \quad Qt & \text{From 6} \\ (9) & \quad \quad \quad \quad P \to Qt & \to-\text{Elim 7 to 8} \\ (10) & \quad \quad \quad \quad \bot \\ \\ (11) & \quad \quad \quad \quad P & \text{Assumption} \\ (12) & \quad \quad \quad \quad \exists x ~ Qx & \text{From 2 and 6} \\ (13) & \quad \quad \quad \quad \bot & \exists-\text{Elim of 12 and 6 to 10} \\ (14) & \quad \quad \quad \quad Qx & \text{From 13} \\ \\ (15) & \quad \quad P \to Qx & \to-\text{Elim of 11 to 14} \\ (16) & \quad \quad \exists x ~ (P \to Qx) & \text{From 15} \\ \\ (17) & \exists x ~ (P \to Qx) & \lor-\text{Elim, 1, 3 to 4, 5 to 16} \end{array}$$