Consequentia mirabilis

Consequentia mirabilis (Latin for "admirable consequence"), also known as Clavius's Law, is used in traditional and classical logic to establish the truth of a proposition from the inconsistency of its negation. It is thus related to reductio ad absurdum, but it can prove a proposition using just its own negation and the concept of consistency. For a more concrete formulation, it states that if a proposition is a consequence of its negation, then it is true, for consistency. In formal notation:

${\displaystyle (\neg A\to A)\to A}$.

Weaker variants of the principle are provable in minimal logic, but the full principle itself is not provable even in intuitionistic logic.