Thread: 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

Good question. Classical reasoning in natural deduction may be nonobvious. I'll describe it informally at first. I believe you can use double-negation elimination rule (DNE), which derives Q from ~~Q.

Assume ~(P \/ ~P). Then assuming P leads to a contradiction, so ~P. However, this also leads to a contradiction. Thus, ~~(P \/ ~P), from where you get P \/ ~P by DNE.

Thank you emakarov, great help! Problem solved

I assume the formal system you want to use is natural deduction in the classical sense. Intuitionist logic, for instance, has problems with negation elimination rules, which results in questioning the law of excluded middle (LEM) altogether. In such a system, there would be no formal proof of the LEM. Instead, you could prove in that system up to step 7 below.

0 | ¬(p v ¬p) [assumption]
1 || p [assumption]
2 || p v ¬p [disjunction introduction, 1]
3 || FALSE [contradiction, 0 2]
4 | ¬p [negation introduction, 1-3]
5 | ¬p v p [disjunction introduction, 4]
6 | FALSE [contradiction, 0 5]
7 ¬¬(p v ¬p) [negation introduction, 0-6]
8 p v ¬p [negation elimination, 7]

Notice how everything up to step 8 was either an assumption or an introduction rule. Also notice that the only two lines that had their assumptions terminated (no spacer lines at the beginning) are the last two. The intuitionist has no problem with everything up to 7. The problem is only in the last step. In that step we have to eliminate the negations. For the intuitionist, p → ¬¬p, but they disallow ¬¬p → p, which by that and modus ponens would give us 8. Classically all statements are taken to possess either a true or false truth value. Thus, the LEM has to obtain because something either is or it is not, classically. However, other systems like intuitionism takes truth to be congruent with construction. Something is true only if we can define an algorithm or process to produce it. A sentence is false if its assumption leads to a contradiction. Classically, the law of double negation (negation elimination) says that both the above implications holds. Thus p is equivalent to ¬¬p. Therefore, we can conclude 8 by the above natural deduction proof.

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.

Spoonwood, welcome to the forum.

Could you clarify your notation? I am not sure what A, K and N mean.

Originally Posted by emakarov

Spoonwood, welcome to the forum.

Could you clarify your notation? I am not sure what A, K and N mean.

Sure, sorry about that. "A" stands for alternation, or equivalently disjunction. In classical (2-valued logic) if Axy is true, then at least one of the alternates "x" or "y" is true. One might also say that if Axy is true, then either x is true, otherwise y is true. The term "alter" basically means "other", hence alternation. "K" stands for conjunction. In Polish, Jan Lukasiewicz a Pole invented this notation, the English word "conjunction" gets translated as "konjunction". Also, read aloud, the "c" in conjunction has a hard "k" sound to it. N stands for negation.

So, in a more standard infix notation one might write Kxy as (x^y), Axy as
(x v y), and Nx as ~(x). Actually, ~(x) isn't in infix notation, it comes in prefix notation. Unary functions, operations, and connectives simply don't exist in prefix (or suffix) notation since you need two symbols for an infix notation.