Formal proof for P → Q ≡ ¬P ∨ Q in Fitch

Question

I'm trying to construct a formal proof for 'P → Q ≡ ¬P ∨ Q' in Fitch. I know this is true, but how do I prove it?

Would you consider a truth table as a proof? – AngryOliver Sep 19 '14 at 18:41 — AngryOliver, Sep 19 '14 at 18:41
No, I'm looking for a formal proof in Fitch. – Yaeger Sep 19 '14 at 18:41 — Yaeger, Sep 19 '14 at 18:41

score 4 · Accepted Answer · edited Feb 08 '17 at 14:56

4

I finally managed to solve it:

enter image description here

fairly straight forward actually

edited Feb 08 '17 at 14:56

Community

1
1

answered Sep 19 '14 at 21:39

Yaeger

253
4
15

score 1 · Answer 2 · answered Jan 17 '17 at 14:30

Given p ⇒ q, use the Fitch System to prove ¬p ∨ q.

1.  p => q            Premise
2.    ~(~p | q)       Assumption
3.      ~p            Assumption
4.      ~p | q        Or Introduction: 3
5.    ~p => ~p | q    Implication Introduction: 3, 4
6.     ~p             Assumption
7.     ~(~p | q)      Reiteration: 2
8.    ~p => ~(~p | q) Implication Introduction: 6, 7
9.    ~~p             Negation Introduction: 5, 8
10.   p               Negation Elimination: 9
11.   q               Implication Elimination: 1, 10
12.   ~p | q          Or Introduction: 11
13. ~(~p | q) => ~p | q        Implication Introduction: 2, 12
14.  ~(~p | q)                 Assumption
15. ~(~p | q) => ~(~p | q)     Implication Introduction: 14, 14
16. ~~(~p | q)                 Negation Introduction: 13, 15
17. ~p | q                     Negation Elimination: 16

Goal ~p | q Complete

Formal proof for P → Q ≡ ¬P ∨ Q in Fitch

2 Answers2