It's all in the question really. I am working on a proof in Fitch for a class, but I am very much stuck.

I am proving the tautology that "(P → Q) ↔ (¬P ∨ Q)", and I have already finished half of it, but now I must prove that "(¬P ∨ Q)" implies "(P → Q)". I can't seem to get anywhere.

I try to set up a proof by cases where I assume in different subproofs "¬P" and (in the other) "Q", but then I must prove "P → Q" from those. It seems even more difficult. Any help would be appreciated.


You are right : the correct way is to use proof by cases:

1) Q --- assumed for the proof by cases [a-1]

2) P → Q --- from 1) by -intro

3) ¬P --- assumed for the proof by cases [a-2]

4) P --- assumed [b]

5) contradicition !

6) Q --- from 5)

7) P → Q --- from 6) by -intro, discharging [b]

and it is done.

  • In step two, I am not sure how you can use →-intro for that. For →-intro you need to point to a subproof with premise p and conclusion q, do you not? In my fitch program it does not allow that move. Futhermore, I am not sure how you obtained p in step 4, is it a second assumption of the subproof? – Zenreon Nov 21 '16 at 0:36
  • @Zenreon - to "bypass" Fitch, 1) start a subproof with assumption P, then assume Q, then →-intro discharging P. – Mauro ALLEGRANZA Nov 21 '16 at 6:52

Using the Fitch-style natural deduction proof editor and checker I can write the following proof:

enter image description here

Line 1 contains the premise.

Since we ultimately want upon assuming "P" to get "Q", I assume "P" on line 2 by starting a subproof which according to the Fitch notation is indented.

In order to get a contradiction I start another subproof and assume "¬Q" in line 3.

In line 4, I use the disjunctive syllogism (DS) rule. I have a disjunction, "¬P ∨ Q", and "¬Q". I can conclude by disjunctive syllogism "¬P". See forall x: Calgary Remix, pages 124-5, for a description of this rule.

In line 5, I introduce a contradiction (⊥) due to lines 2 and 4.

The contradiction completes an indirect proof (IP) which allows me to close the subproof discharging the assumption, "¬Q", on line 6.

In line 7, I introduce a conditional from lines 2 through 6 which completes the proof.


Since you seek to prove that a disjunction entails a conditional, therefore your strategy ought be to: use disjunction elimination and, in each case, conditional introduction, if you can.

|_ ~p v q         : premise
|  |_ ~p          : assumed case 1
|  |  |_ p        : assumption
|  |  |           : ...
|  |  |  q        : ...
|  |  p -> q      : conditional introduction (...)
|  ~p -> (p -> q) : conditional introduction (...)
|  |_ q           : assumed case 2
|  |  |_ p        : assumption
|  |  |           : ...
|  |  |  q        : ...
|  |  p -> q      : conditional introduction (...)
|  q -> (p -> q)  : conditional introduction (...)
|  p -> q         : disjunction elimination (...)

Then it is just a matter of deciding whether p would imply q under each from the two cases, and how if so.

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.