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:









  • $\begingroup$ Can you use that the existential quantifier distribute over disjunction? $\endgroup$
    – aduh
    Jan 5, 2018 at 16:10
  • $\begingroup$ @aduh, I can use it if I can prove it within the actual proof, as everything needs to be derived using the basic introduction and elimination rules. $\endgroup$
    – RTK
    Jan 5, 2018 at 17:05

3 Answers 3


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)).$

  • $\begingroup$ The use of $\to$-intro while $c$ is outstanding hides a nonconstructive inference. $\endgroup$
    – DanielV
    Jan 5, 2018 at 20:23
  • $\begingroup$ This can't be right. You have only mentioned intuitionistically valid inference rules. But the target result is not intuitionistically valid. $\endgroup$ Jan 5, 2018 at 20:23
  • $\begingroup$ @PeterSmith No the $\to$ intro is not intuitionistically valid because he is using the "constants" version of $\exists$-elim instead of the "proof by cases" version of it. $\endgroup$
    – DanielV
    Jan 5, 2018 at 20:29
  • $\begingroup$ Fair enough but then he's changed the subject. The question was to give a proof using "only the basic introduction/elimination rules from used in Fitch." and that's a proof-by-cases rule. $\endgroup$ Jan 5, 2018 at 20:32
  • 1
    $\begingroup$ @spaceisdarkgreen I think your answer is correct. In fact for a nonlogician I would prefer it, since I wouldn't want a beginner student to get caught up in issues of constructivism. I was pointing out what I said because someone may wonder "why is the other proof so much more complicated". What you said about isolating LEM is correct. $\endgroup$
    – DanielV
    Jan 5, 2018 at 21:36

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}$$


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:

enter image description here

  • $\begingroup$ This proof has three odd features (NOT a complaint about Bram's derivation but about the system we are working with!!) (i) It involves explosion, at (6). (ii) It involves vacuous/irrelevant discharge, at (16). (iii) Although we know we must use $\neg$Elim as the theorem doesn't hold in intuitionist logic, it seems odd to have to use it twice. Raises the question of what more natural Natural Deduction rules would give a more intuitive proof. $\endgroup$ Jan 5, 2018 at 19:41
  • $\begingroup$ @PeterSmith Well one way to inspect that question is to try to prove $P \to (A \lor B) \vdash (P \to A) \lor (P \to B)$ and see if you can do it with only 1 instance of LEM. $\endgroup$
    – DanielV
    Jan 5, 2018 at 20:36
  • $\begingroup$ Well, yes: suppose $\neg((P \to A) \lor (P \to B))$; suppose $P$. Then use $A \lor B$ in argument by cases for $\bot$, proving $\neg P$. Use that to prove $(P \to A)$, hence contradiction with first supposition. Assuming usual explosion rule. (No? ;)) $\endgroup$ Jan 5, 2018 at 20:43
  • $\begingroup$ @PeterSmith Well that's it then, done with only 1 instance of LEM. Do you want to write it up? It is a very short proof. $\endgroup$
    – DanielV
    Jan 5, 2018 at 20:51
  • $\begingroup$ @PeterSmith There are some things I want to say about constructive reasoning so I'll just write it up if that is ok with you~ $\endgroup$
    – DanielV
    Jan 5, 2018 at 21:11

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .