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.
[1] 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: Weaker variants of the principle are provable in minimal logic, but the full principle itself is not provable even in intuitionistic logic.
"[2] Barnes claims in passing that the term consequentia mirabilis refers only to the inference of the proposition from the inconsistency of its negation, and that the term Lex Clavia (or Clavius' Law) refers to the inference of the proposition's negation from the inconsistency of the proposition.
[3] The following shows what weak forms of the law still holds in minimal logic, which lacks both excluded middle and the principle of explosion.
Frege's theorem states For
this is a form of negation introduction, and then for
and using the law of identity, it reduces to Now for
By implication introduction, this is indeed an equivalence, In minimal logic, the first double-negation in the original implication can optionally also be removed, weakening the forward direction statement to
Of course, when adopting the double-negation elimination principle for all propositions, consequentia mirabilis also follows simply because the latter brings minimal logic back to full classical logic.
This shows that already minimal logic validates that a proposition
cannot be rejected exactly if this is implied by its negation, and that
can also be seen to be equivalent to the principle of non-contradiction
To this end, first note that using modus ponens and implication introduction, the latter principle is equivalent to
, i.e. the fact that there are equivalent characterizations of two propositions being mutually exclusive.
The negation of any excluded middle disjunction
From the above weak form, it thus follows that any double-negated excluded middle statement is valid, in minimal logic.
Likewise, this argument shows how the full consequentia mirabilis implies excluded middle.
The following argument shows that the converse also holds.
A principle related to case analysis may be formulated as such: If both
, the principle of identity now entails Whenever the second conjunct of the antecedent,
, is true, then so is the instance of the principle.
By conjunction elimination, this is in fact an equivalence.
, which gives another demonstration of how double-negation elimination implies consequentia mirabilis, in minimal logic.
In intuitionistical logic, the principle of explosion itself may be formulated as
So here, It was established how consequentia mirabilis follows from double-negation elimination in minimal logic, and how it is equivalent to excluded middle.
, the propositional form of the reverse disjunctive syllogism.
Related to the last intuitionistic derivation given above, consequentia mirabilis also follow as the special case of Peirce's law for
That article can be consulted for more, related equivalences.