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 '17 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 '20 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 '20 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 '17 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 '17 at 2:08
  • I apologize, I used the wrong link. logic.stanford.edu/intrologic/exercises/exercise_04_14.html May 9 '17 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 '17 at 3:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.