I am very new to proof and logic and I would really appreciate a rundown of this proof.

I use a program called Fitch to construct my proofs.

I understand there are two types of proofs. Direct Proofs and Case Proofs.

Please could someone be so kind as to walk me through both types using this example:

Given  P ∨ ¬ P prove  (P → Q) → ((¬ P → Q) → Q)

Following this I have deduced the following but I cannot post this as an answer yet as something doesn't check out.

Any advice why this might be. It seems to make logical sense to me to deduce ∨ elim from these sub-proofs.

enter image description here

  • Welcome to Philosophy.SE! What have you tried yourself? Please edit your question to give your first steps and what specifically you don't understand.
    – user2953
    Sep 11, 2015 at 12:46
  • @Keelan Thanks! My thinking is to break this up into cases i.e. subproofs. I am admittedly not that far into this. I am on line 4 but already at line 3 I am missing something and I just need a bit of guidance in the right direction. Sep 11, 2015 at 12:55
  • so, perhaps you could share these lines (and the rest of the proof) so that we can really help you instead of just giving the answer? Thanks.
    – user2953
    Sep 11, 2015 at 12:56
  • 1
    @Keelan I've edited my question with a snapshot. I would prefer nudges in the right direction as oppose to just the answer. Appreciate the help. Sep 11, 2015 at 12:58
  • thanks! I'm a little busy right now, but will pass by later today and write up an answer if there is none yet.
    – user2953
    Sep 11, 2015 at 13:01

2 Answers 2


1) P ∨ ¬ P --- premise

2) (P → Q) --- assumed [a]

3) (¬ P → Q) --- assumed [b]

4) P --- assumed [c] for ∨-elimination

5) Q --- from 4 and 2 by →-elimination

6) ¬ P --- assumed [d] for ∨-elimination

7) Q --- from 6 and 3 by →-elimination

8) Q --- from 4-5 and 6-7 by ∨-elimination, discharging [c] and [d]

9) (P → Q) → ((¬ P → Q) → Q) --- from 3, 2 and 8 by →-introduction twice, discharging [b] and [a]

P ∨ ¬ P ⊢ (P → Q) → ((¬ P → Q) → Q) --- from 1 and 9.

Side comment : the proof is intuitionistically valid. We can read it as : if we assume the Law of Excluded Middle, then the conclusion follows.

In classical logic the formula (P → Q) → ((¬ P → Q) → Q) is a tautology, and thus provable without assumptions; this is not possible with intuitionistic logic.

  • Many thanks. Your answer looks for easier than mine. Is this an example of a direct proof? I am going to post what I have but there is one mistake re my elim ∨ of a couple of subproofs which isn't checking out. Any thoughts? Sep 11, 2015 at 15:14

My proof with Fitch: https://gyazo.com/00858637c59c1ed8697cb48378dc7ae0 Make sure you understand why I make the specific assumptions. Its important to understand why the proof follows, everytime you understand a new proof you aquire new tools to your "natural deduction toolkit".


You must log in to answer this question.

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