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

Question

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.

Thank you in advance for your help.

Answer 1

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.

Answer 2

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 |
+---+--------------+-------------------------------------------+