# Given P ∨ ¬ P prove (P → Q) → ((¬ P → Q) → Q) by natural deduction

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: 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. • 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 '15 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. – Metamorphosis Sep 11 '15 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 '15 at 12:56
• @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. – Metamorphosis Sep 11 '15 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 '15 at 13:01

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? – Metamorphosis Sep 11 '15 at 15:14

My proof with Fitch: 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".