Introduction to Logic
Given p ⇒ q, use the Fitch System to prove ¬p ∨ q.
Show Instructions
To apply a rule of inference, check the lines you wish to use as premises and click the button for the rule of inference. Reiteration allows you to repeat an earlier item. To delete one or more lines from a proof, check the desired lines and click Delete. When entering expressions, use Ascii characters only. Use ~ for ¬; use & for ∧; use  for ∨; use => for ⇒; use <=> for ⇔.
1
p => q
Premise
2
~(~p  q)
Assumption
3
p
Assumption
4
q
Implication Elimination
1
3
5
~p  q
Or Introduction
4
6
p => ~p  q
Implication Introduction
3
5
7
p
Assumption
8
~(~p  q)
Reiteration
2
9
p => ~(~p  q)
Implication Introduction
7
8
10
~p
Negation Introduction
6
9
11
~(~p  q) => ~p
Implication Introduction
2
10
12
~(~p  q)
Assumption
13
~p
Assumption
14
~p  q
Or Introduction
13
15
~p => ~p  q
Implication Introduction
13
14
16
~p
Assumption
17
~(~p  q)
Reiteration
12
18
~p => ~(~p  q)
Implication Introduction
16
17
19
~~p
Negation Introduction
15
18
20
~(~p  q) => ~~p
Implication Introduction
12
19
21
~~(~p  q)
Negation Introduction
11
20
22
~p  q
Negation Elimination
21
