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

  • 1
    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.
    – virmaior
    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.
    – polcott
    Apr 20, 2020 at 14:33

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

  • 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?
    – virmaior
    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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .