I was doing some exercises in my course book when I came across a weird question. I was asked to prove the validity of the following sequent:
$ \vdash \neg p \to (p \to (p \to q)) $
I'm having trouble understanding the given solution of that exercise:
Specifically, why is the first $p$ assumption not "rejected" as a contradiction, while the second $p$ assumption is?
Any help is appreciated.
You could write the very same proof but instead justify line 4 as "$\neg$e 2,1" -- and that would be equally valid. The author of the proof only just made a random choice of which of the two $p$ assumptions to appeal to. (Both of the assumptions have to be there in order to get two "$p\to$" in the eventual conclusion, but which of them is used for $\neg$e is not important).
Indeed you could then also have chosen to apply the $\neg$e rule before starting the innermost box. That would produce yet a different, still valid, proof.
It also sounds like you're slightly misunderstanding the purpose of the $\neg$e rule. It is not there to "reject" a particular assumption -- indeed its premises need not be assumptions at all; they could be concluded using other rules along the way.
What $\neg$e tells you is just that the totality of all the assumptions you have in play at that point in the proof is contradictory. The proof system doesn't really care to track which of your possibly many assumptions contradict each other; it just concludes that there is a contradiction somewhere.