In Fitch, how does one prove "(P → Q)" from the premise "(¬P ∨ Q)"?

Question

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.

Answer 1

You are right : the correct way is to use Proof by cases (aka: Disjunction elimination):

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

2) P → Q --- from 1) by Conditional introduction

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

4) P --- assumed [b]

5) contradicition !

6) Q --- from 5) by Ex falso

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

and it is done.

Answer 2

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

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.

Answer 3

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        : reiteration (...)
|  |  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.

---

Alternatively, assume p first then use disjunction elimination. [It often turns out to be more efficient to delay DE as long as possible: Build a mountain with two peaks rather than two mountains.]

 |_ ~p v q      : premise
 |  |_ p        : assumption
 |  |  |_ ~p    : assumption
 |  |  |  :     : ...
 |  |  |  q     : ...
 |  |  ~p -> q  : conditional introduction
 |  |  |_ q     : assumption
 |  |  q -> q   : conditional introduction
 |  |  q        : disjunction elimination
 |  p -> q      : conditional introduction