# 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. Mar 5, 2020 at 1:05