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!