= Reductio ad absurdum
{title2=$(\neg P\Rightarrow\bot)\Rightarrow P$}
{wiki}
= Proof by contradiction
{synonym}
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.
Back to article page
