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

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).

• I see... the link has the answer by the way, but the key is the comparatively obtuse rule of en.wikipedia.org/wiki/Negation_introduction combined with conditional proofs. May 9, 2017 at 2:31
• Virmaior, I don't get how do you go from 9. ¬(p ∨ ¬p) -> ¬p to X. ¬(p ∨ ¬p) -> ¬¬p Could you please explain? Thank you
– Luen
Apr 20, 2020 at 14:07
• "(Note that the fitch system lacks contradiction elimination (RAA) as a method for getting out of assumptions)." That seems like a horribly stupid limitation. Apr 20, 2020 at 14:33

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.

• I cannot use the contradiction elimination as per the rules in the link I provided. May 9, 2017 at 2:02
• when I go to the link, I get "Error: Sorry, there was an error connecting you to the application.Invalid or missing lti_message_type parameter." ... can you list your rules? May 9, 2017 at 2:08
• I apologize, I used the wrong link. logic.stanford.edu/intrologic/exercises/exercise_04_14.html May 9, 2017 at 2:10
• It worked! I appreciate the help. I felt like it had to be similar to how question 13 was done, but I didn't know to start with the assumption of ~(p | ~p) rather than starting with just the assumption of p and using an or introduction to start. May 9, 2017 at 3:06