# Use the Fitch system to prove the tautology (p ∨ ¬p). Stalled for days (NOT duplicated)

First of all, please don't close this question cause I don't get the explanation given in: Use the Fitch system to prove the tautology (p ∨ ¬p)

I have been trying to solve this exercise for days now. I'm stuck in step 9:

Any thoughts? Thank you.

• Why do you think that is not a duplicate ? In the linked post there is a Fitch proof: instead of retrying with a new post, why not checking it ? Commented Apr 20, 2020 at 15:13
• You step 4 is the wrong one: use the contradiction with 1 and 3 to derive not-p. Commented Apr 20, 2020 at 15:14
• The explanation Virmaior gives is very unclear and it is 3 years old. I haven't been able to solve it based on his explanation. That's why I need a new input.
– Luen
Commented Apr 20, 2020 at 15:15
• Having derived not-p, you discharge 1 to get : not-(p or not-p) to not-p. Having done so, repeat all the derivation from 1 with the new assumption not-p in 2. In this case you get not-(not-p) and discharge again the assumption to get: not-(p or not-p) to not-(not-p). Now you can apply negation-intro rule (as above) to conclude with not-( not-(p or not-p) ). Commented Apr 20, 2020 at 16:08
• Step 12 is same as 3 and 4 will be not-p to (p or not-p). And so on. Commented Apr 20, 2020 at 16:31