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 '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
  • 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. – 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.

| improve this answer | |
  • 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: 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".

| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.