What would a formal Fitch proof for this look like?

I am given ¬∀x(P(x)→Q(x)), and need to derive ∃xP(x) from it.

I started with this, but I don't know if I am doing the right thing, and where to go from there:

enter image description here

EDIT: Did it (see answer)

  • So far no answers written out in English. Isn't the crux of the matter that if there were no $x$ such that $P(x)$, then $P(x)$ would be false for all $x$ and thus would imply absolutely anything?
    – Wildcard
    Nov 26, 2018 at 5:33

4 Answers 4


Resolved! I realised that I was going nowhere by assuming the opposite of what I was given as premise... I obviously had to assume the opposite of what I was trying to prove:

enter image description here

  • Indeed. You have a correct solution. You can now accept your own answer to close this question. Nov 25, 2018 at 22:38

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

2) ¬∃xP(x) --- assumed [a]

3) P(x) --- assumed [b]

4) ∃xP(x) --- from 3) by -intro

5) --- contradiction : from 2) and 4)

6) Q(x) --- from 5) by -elim

7) P(x) → Q(x) --- from 3) and 6) by -intro, discharging [b]

8) ∀x(P(x) → Q(x)) --- from 7) by -intro

9) --- contradiction : from 1) and 8)

10) ∃xP(x) --- from 2) by Double Negation (or ¬-elim), discharging [a].


The following proof is the same as Mauro ALLEGRANZA's but it uses Klement's Fitch-style proof checker. Descriptions of the rules are in forallx. Both are available online and listed below. They may help as supplementary material to what you are currently using.

You may be required in your proof checker to represent contradictions as conjunctions of contradictory statements. This proof checker only requires noting the contradiction as "⊥" and listing the contradictory lines such as I did on lines 5 and 9.

enter image description here


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

  • I managed to do it, but my result is slightly different from yours. I tried yours out of curiosity, and it does not work in the Fitch program I have. I'm puzzled by the fact that your proof checker allowed you to export the temporary assumption 'a' outside of its subproof!
    – 35308
    Nov 25, 2018 at 21:07
  • @35308 You could look at that subproof (lines 3-6) as saying the same thing as the conditional statement on line 7 "Pa > Qa". Given the assumption Pa, I can derive Qa with what is available (namely line 2). The subproof just showed how that was done and the proof checker required that I show that before using line 7. Nov 25, 2018 at 21:21
  • The issue is that you really should not be allowed to introduce a new free term 'a' without raising a new context to isolate it. Nov 25, 2018 at 22:48

Pr. ~∀x(P(x)->Q(x))

2.∃x~(P(x)->Q(x)) ~ Universal out Pr.

3.~(P(a)->Q(a)) Existential out (x/a) 2

4.P(a)&~Q(a) ~ conditional out 3

5.P(a) Conjunction out 4

6.∃xP(x) Existential In 5

You must log in to answer this question.

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