Is my natural deduction proof correct?
- by Danny King
Hello,
Given the sequent:
|- p v ¬p
(that is, no left-hand-side, derives p or not p)
I have taken this from http://www.danielclemente.com/logica/dn.en-node38.html but I got a different proof to his solution.
I think my simpler proof is correct but could someone verify it for me to check I have understood it? I'd appreciate it very much!
1. ¬(p v ¬p) assumption {note this is equivalent to ¬p ^ p}
2. ¬p ^elimination 1
3. p ^elimination 1
4. contradiction ¬elimination 3, 2
5. p v ¬p ¬introduction 1-4
Thanks!