Formal proof of "Law of ecxluded middle"
I wonder how to give a formal, Fitch-style, proof of P v P ..?
I am able to prove it by contradiction when I use that P & P is a tautological consequence of (P v P ) . But in order to prove this (one of the DeMorgan's laws I think?) formally I have to use the law of excluded middle itself...
I also know how to show these tautologies with truth tables, but an exercise explicitly ask for a formal proof of P v P .
All help is appreciated :)
A shorter proof of the formal law of the excluded middle
A shorter way to construct a proof here comes as to use a rule of single-negation elimination instead of double-negation elimination... "From a sub-derivation which starts with Np and derives a contradiction, we may immediately infer p." Jaskowski, one of the founders of natural deduction, and whose proof boxes lead to Fitch-style proofs, used this rule instead of double-negation elimination. But, I digress. In prefix notation a proof can go:
0 | NApNp hypothesis
1 || Np hypothesis
2 || ApNp 2 alternation introduction
3 || KApNpNApNp 3, 1 conjunction introduction
4 | p 2-4 negation elimination
5 | ApNp 5 alternation-introduction
6 | KApNpNApNp 6, 1 conjunction introduction
7 ApNp 1-7 negation elimination
This does hold in some non-classical logics, and works as a proof in any non-classical logic where the rules of inference here used here work out as sound. If you want to consider all non-classical logics at once, this formal law neither holds nor does not hold.