PfPrintForm Definitions LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Thm*  (P  P)

That is, no proposition is equivalent to its own negation.

Proof:

Suppose P  P.

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:
prop
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PfPrintForm Definitions LogicSupplement Sections DiscrMathExt Doc