I'm taking a course from Stanford in Logic. I'm stuck with an exercise where I'm doing some proof. The Fitch system I'm given only allows
- $ \land $ introduction and elimination
- $ \lor $ introduction and elimination
- $ \to $ introduction and elimination
- $ \equiv $ introduction and elimination
- $ \lnot$ introduction and
- $ \lnot \lnot $ elimination
but not
- $ \bot $ introduction and elimination
I've been struggling to prove the law of excluded middle (“p ∨ ¬p`) within this system. All of the proofs I've seen online make use of $\bot$ elimination to prove it by contradiction:
| ~(p | ~p) (assumption)
| | p (assumption)
| | p | ~p (or introduction)
| | $\bot$
|
| | ~p (assumption)
| | p | ~p (or introduction)
| | $\bot$
|
| (p | ~p) (proof by contradiction)
Since I can't use $\bot$ elimination, I was trying to do this with $ \lnot$ introduction:
| ~(p | ~p) (assumption)
| | ???
| ~(p | ~p) => x
|
| | ???
| ~(p | ~p) => ~x
| p | ~p (not introduction)
but I just can't get it. I can't figure out how to get x
and ~x
.
Is this provable without $\bot$ elimination? If so, what are the steps?
Background:
What I'm ultimately trying to prove is this: Given p ⇒ q, use the Fitch System to prove ¬p ∨ q.
I'm able to prove that p ⇒ ¬p ∨ q
and that ¬p ⇒ ¬p ∨ q
, but I need to be able to plug p ∨ ¬p
into the proof to be able to do 'or elimination'.
Best Answer
1) $\lnot (A \lor \lnot A)$ --- assumed [a]
2) $A$ --- assumed [b]
3) $A \lor \lnot A$ --- from 1) by $\lor$-intro
4) $\lnot A$ --- from the contradiction : 2) and 3) by $\lnot$-intro, discharging [b]
5) $A \lor \lnot A$ --- $\lor$-intro
6) $\lnot \lnot (A \lor \lnot A)$ --- from the contradiction : 1) and 5) by $\lnot$-intro, discharging [a]
For the different "flavours" of the negation rules in Natural Deduction you can see :
Dag Prawitz, Natural Deduction : A Proof-Theoretical Study (1965), page 35 (for the two $\lnot$-rules replacing the $\bot$-rules in classical logic); or :
Neil Tennant, Natural logic (1978), page 57.
Your idea regarding the proof : $P \to Q \vdash \lnot P \lor Q$ is correct: you can use the "derived" rule :
Alternatively :
0) $A \to B$ --- premise
1) $\lnot A$ --- assumed [a]
2) $\lnot A \lor B$ --- by $\lor$-intro
3) $\lnot (\lnot A \lor B)$ --- assumed [b]
4) $\lnot \lnot A$ --- from 1) with contradiction : 2) and 3) by $\lnot$-intro, discharging [a]
5) $A$ --- from 4) by $\lnot \lnot$-elim
6) $B$ --- from 0) and 5) by $\to$-elim
7) $\lnot A \lor B$ --- $\lor$-intro
8) $\lnot \lnot (\lnot A \lor B)$ --- from 3) with contradiction : 7) and 3) by $\lnot$-intro, discharging [b]
9) $\lnot A \lor B$ --- from 8) by $\lnot \lnot$-elim
Thus, from 0) and 9) :