# How can I prove the law of excluded third (p ∨ ¬p)) using Fitch?

Good day. I do not quite understand how I can get ~~p after the 11th line.

According to the proof of the law itself (and all reasonable logic) I should get it, and then simplify the expression - but I can not do it.

Good day. I do not quite understand how I can get ~~p after the 11th line.

Good day. You do not necessarily require ~~p to contradict ~p, you simply need some contradiction to be derivable from assuming ~(p | ~p). Well, (p | ~p) contradicts the assumption itself, so...

Don't reiterate on line 10. The sub-proof is complete (for your purpose) at line 9.

 Line 1  |_ ~(p | ~p)               Assumption
:  :                          : as you had.
Line 9  |  (p | ~p)                Or Introduction  8


From here the next line is instead conditional introduction.

 Line 10 ~(p | ~p) => (p | ~p)      => Introduction  1-9


After this, if only you could somehow derive ~(p | ~p) => ~(p | ~p) then you may apply the Stanford Fitch system's rule of negation introduction, and finally negation elimination (which is more commonly known as double negation elimination).

Somehow… Hmmm …

Anyhow, in your other system, what we have so far should translate to something like:

 U.         ~(p v ~p), p  |-    p             S1
Rv+(S1)    ~(p v ~p), p  |-    p v ~p        S2
U.         ~(p v ~p), p  |-  ~(p v ~p)       S3
R~+(S2,S3) ~(p v ~p)     |-   ~p             S4
Rv+(S4)    ~(p v ~p)     |-    p v ~p        S5


And you can complete this in three more lines.

I have written a proof of P or (not P)

First, a lemma:

LEMMA A   P --> (P or (not P))
+---+--------------+----------------------------+
| 1 |      P       |         assumption         |
+---+--------------+----------------------------+
| 2 | P or (not P) | line 1, introduction of or |
+---+--------------+----------------------------+


then another lemma:

LEMMA B   not P --> (P or (not P))
+---+--------------+----------------------------+
| 1 |      not P   |         assumption         |
+---+--------------+----------------------------+
| 2 | P or (not P) | line 1, introduction of or |
+---+--------------+----------------------------+


Finally, the theorem:

THEOREM "Bob"  .........  P or (not P)
+---+--------------+-------------------------------------------+
| 1 | P or (not P) | from lemma A, lemma B, and proof by cases |
+---+--------------+-------------------------------------------+

• No, you cannot use Proof by Cases for this. Such a proof takes the form of: A v B, A => C, and B => C entails C. Now, you have proven the two conditionals, P => P v ~P and ~P => P v ~P. However you have not yet proven the disjunction P v ~P because that is that you are trying to prove. Commented Mar 5, 2020 at 1:05