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'.