IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Thm* (PP)
That is, no proposition is equivalent to its own negation.
Proof:
Suppose PP.
Then P, since assuming P for the sake of argument would allow us to conclude P, contradicting the assumption P.
But from P, P itself now follows.
Sidenote:
Sometimes this theorem is proved considering both cases of P being true or false, and showing that each way leads to a contradiciton.
In contrast there is no case splitting in the argument shown here, just an argument that P would be false and therefore also true.
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html