Use the Fitch system to prove the tautology (p ∨ ¬p)

Question

I've scoured the math stackexchange and the philosophy one for some guidance on how to go about this while using the Fitch System.

Anyone can attempt it here; http://logic.stanford.edu/intrologic/exercises/exercise_04_14.html

I can reach the conclusion, but it's not in the correct "layer" of the proof. I'm stuck with the answer as a subproof.

(Note that the fitch system lacks contradiction elimination (RAA) as a method for getting out of assumptions).

Answer 1

Outside of fitch, conceptually the answer is as follows:

1. | ¬(p ∨ ¬p)   A
2. | | p         A
3. | | p ∨ ¬p    vI 2
4. | | ¬(p ∨ ¬p) R 1
5. | ¬p          Contradiction Elim. 3,4 (2-4)
6. | p ∨ ¬p      v5
7. p ∨ ¬p        Contradiction Elim. 1,6 (1-6)

and there you go.

The hard part is that fitch lacks contradiction elimination. Instead, you need to use Negation Introduction, here's how you do that for the top half:

1. | ¬(p ∨ ¬p)   A
2. | | p         A
3. | | p ∨ ¬p    vI 2
4. | p -> (p ∨ ¬p) Imp. Introduction 2,3
5. | | p         A
6. | | ¬(p ∨ ¬p) R 1
7. | p -> ¬(p ∨ ¬p)  Imp. Introduction 5,6
8. | ¬p          Neg. Intro. 4,7

Then drop down an assumption by imp introduction:

9. ¬(p ∨ ¬p)  -> ¬p

repeat the same thing as above but with not ¬p yielding

X. ¬(p ∨ ¬p)  -> ¬¬p
Y. ¬¬(p ∨ ¬p) Neg. Intro 8 + X
Z. p ∨ ¬p   DN Y

To explain it a little bit conceptually, Contradiction Elimination says "we have hit a contradiction in this sub proof so we reject its assumption." Negation Introduction says "if this antecedent were true, we would hit a contradiction because this antecedent implies contradictory outcomes, so the antecedent is false." In other words, it is a way of eliminating contradictions by denying the assumptions that go to them.

In a sense, the "negation elimination" approach is more careful about handling the principle of explosion, but it's effect is the same in proving -- it's just more painful to write them out.