Consequentia mirabilis

Template:Short description Template:Italic title 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:

$(\mathrm{\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.

History

Consequentia mirabilis was a pattern of argument popular in 17th-century Europe that first appeared in a fragment of Aristotle's Protrepticus: "If we ought to philosophise, then we ought to philosophise; and if we ought not to philosophise, then we ought to philosophise (i.e. in order to justify this view); in any case, therefore, we ought to philosophise."

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.

Derivations

The first demonstration purposely makes use of only rather conservative logical assumptions, up to the last step:

Firstly, that implications can be chained together to obtain yet another one is a consequence of Frege's theorem. This states

$(B\to (C\to D))\to ((B\to C)\to (B\to D))$

For $D=\mathrm{\perp }$ reduces to a form of negation introduction, and indeed for further $B=C$ and using the law of identity, one obtains

$(B\to \mathrm{\neg }B)\to \mathrm{\neg }B$

Now for $B=\mathrm{\neg }A$, it follows that $(\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }A)\to \mathrm{\neg }\mathrm{\neg }A$. By implication introduction, this is indeed an equivalence,

$(\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }A)\leftrightarrow \mathrm{\neg }\mathrm{\neg }A$.

Minimal logic lacks excluded middle and the principle of explosion. But already here, the first double-negation in the original implication can optionally also be removed, weakening the forward direction statement to

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

Hence, consequentia mirabilis thus holds whenever $\mathrm{\neg }\mathrm{\neg }A\leftrightarrow A$.

Minimal logic

The variant with the equivalence above shows that minimal logic validates that a proposition $A$ cannot be rejected ($\mathrm{\neg }\mathrm{\neg }A$) exactly if this is implied by its negation ($\mathrm{\neg }A\to \mathrm{\neg }\mathrm{\neg }A$). Further, that $A$ holds exactly when it is implied by both $\mathrm{\neg }A$ and $\mathrm{\neg }\mathrm{\neg }A$.

The weak form $(\mathrm{\neg }A\to A)\to \mathrm{\neg }(\mathrm{\neg }A)$ can also be seen to be equivalent to the principle of non-contradiction $\mathrm{\neg }(A\wedge \mathrm{\neg }A)$. To this end, first note that using modus ponens and implication introduction, the latter principle is equivalent to $\mathrm{\neg }((\mathrm{\neg }A\to A)\wedge (\mathrm{\neg }A))$. The claim now follows from $(B\to \mathrm{\neg }C)\leftrightarrow \mathrm{\neg }(B\wedge C)$, i.e. the fact that there are equivalent characterizations of two propositions being mutually exclusive.

Equivalence to excluded middle

The negation of any excluded middle disjunction $B\vee \mathrm{\neg }B$ in particular implies $\mathrm{\neg }B$, and thus the weaker disjunction $B\vee \mathrm{\neg }B$ itself. 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 $B$ and $C$ each imply $A$, and either of them must hold, then $A$ follows. Formally,

$((B\to A)\wedge (C\to A)\wedge (B\vee C))\to A$

For $B=A$ and $C=\mathrm{\neg }A$, the principle of identity now entails

$((\mathrm{\neg }A\to A)\wedge (A\vee \mathrm{\neg }A))\to A$

Whenever the second conjunct of the antecedent, $A\vee \mathrm{\neg }A$, is true, then so is the instance of the principle.

Intuitionistic logic

One has that $(A\to B)\to A$ implies $(A\to B)\to (A\wedge B)$. By conjunction elimination, this is in fact an equivalence. In particular, one has

$(\mathrm{\neg }A\to A)\leftrightarrow (\mathrm{\neg }A\to (A\wedge \mathrm{\perp }))$

The right hand of this also implies $\mathrm{\neg }\mathrm{\neg }A$, which gives another demonstration of how double-negation elimination implies consequentia mirabilis, in minimal logic.

The principle of explosion itself may be formulated as $\mathrm{\perp }\to (A\wedge \mathrm{\perp })$, and therefore $\mathrm{\perp }\leftrightarrow (A\wedge \mathrm{\perp })$. As explosion is valid in intuitionistic logic, here the above reduces to an equivalence,

$(\mathrm{\neg }A\to A)\leftrightarrow \mathrm{\neg }\mathrm{\neg }A$

For what it's worth, this also gives a derivation of double-negation elimination for statements that have already been rejected. In other words, in intuitionistic logic $\mathrm{\neg }A⊢\mathrm{\neg }\mathrm{\neg }A\to A$. Compare this with explosion in general.

Further classical derivations

Above it was established how consequentia mirabilis is equivalent to excluded middle over minimal logic.

A quick derivation from double-negation elimination was demonstrated as well. What follows is two more lines or reasoning:

• When excluded middle holds for $A$, one contraposition gives $(B\to A)\to (A\vee \mathrm{\neg }B)$, the propositional form of the reverse disjunctive syllogism. The law is now obtained with $B=\mathrm{\neg }A$ and, again, double-negation elimination.
• Related to the last intuitionistic derivation given above, consequentia mirabilis also follows as the special case of Peirce's law $((A\to B)\to A)\to A$ for $B=\mathrm{\perp }$. That article can be consulted for more, related equivalences.

See also

• Ex falso quodlibet
• Tertium non datur