Reductio ad absurdum ($(\neg P\Rightarrow \perp )\Rightarrow P$)

A reductio rejects an assumption by deriving an absurd or contradictory consequence from it. In a classical mathematical proof of $P$, assume its negation and derive a contradiction. Constructively the same argument yields the double negation of $P$; removing it requires an additional logical principle. This differs from proving a negation directly by deriving a contradiction from the positive assumption.