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.^[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:

(\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 edit

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."^[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]

Derivations edit

Minimal logic edit

The following shows what weak forms of the law still holds in minimal logic, which lacks both excluded middle and the principle of explosion.

Weaker variants edit

Frege's theorem states

{\big (}B\rightarrow (C\to D){\big )}\to {\Big (}(B\rightarrow C)\to (B\to D){\Big )}

For $D=\bot$ this is a form of negation introduction, and then for $B=C$ and using the law of identity, it reduces to

{\big (}B\rightarrow \neg B{\big )}\rightarrow \neg B

Now for $B=\neg A$ , it follows that

(\neg A\to \neg \neg A)\to \neg \neg A

The first double-negation can optionally also be removed, weakening the statement. As $E\to \neg \neg A$ is always also still equivalent to $\neg \neg (E\to A)$ in minimal logic, the above also constructively establishes the double negation of consequentia mirabilis.

Consequentia mirabilis thus holds whenever $\neg \neg A\leftrightarrow A$ . When adopting the double-negation elimination principle for all propositions, it follows also simply because the latter brings minimal logic back to full classical logic.

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

So minimal logic validates that $A$ holds exactly when it is implied by both $\neg \neg A$ and $\neg A$ .

Equivalence to excluded middle edit

The negation of any excluded middle disjunction implies the disjunction itself. From the above weak form, it thus follows that the 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,

{\big (}(B\to A)\land (C\to A)\land (B\lor C){\big )}\to A

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

{\big (}(\neg A\to A)\land (A\lor \neg A){\big )}\to A

Intuitionistic logic edit

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

{\big (}\neg A\to A{\big )}\leftrightarrow {\big (}\neg A\to (A\land \bot ){\big )}

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

To demonstrate that the principles are in fact equivalent in intuitionistical logic, one needs to show that their antecedants are fully equivalent. Hence, what is to prove is $\bot \leftrightarrow (A\land \bot )$ . This holds because the principle of explosion itself may be formulated as $\bot \to (A\land \bot )$ .

Classical logic edit

It was established how consequentia mirabilis follows from double-negation elimination in minimal logic, and how it is equivalent to excluded middle. Indeed, it may also be established by using the classically valid propositional form of the reverse disjunctive syllogism $(B\to A)\to (\neg B\lor A)$ chained together with the double-negation elimination principle in the form $(\neg \neg A\lor A)\to A$ .

Related to the last intuitionistic derivation given above, consequentia mirabilis also follow as the special case of Pierce's law

{\big (}(A\to B)\to A{\big )}\to A

for $B=\bot$ . That article can be consulted for more, related equivalences.

References edit

^ Sainsbury, Richard. Paradoxes. Cambridge University Press, 2009, p. 128.
^ Kneale, William (1957). "Aristotle and the Consequentia Mirabilis". The Journal of Hellenic Studies. 77 (1): 62–66. doi:10.2307/628635. JSTOR 628635. S2CID 163283107.
^ Barnes, Jonathan. The Pre-Socratic Philosophers: The Arguments of the Philosophers. Routledge, 1982, p. 217 (p 277 in 1979 edition).

[1] Sainsbury, Richard. Paradoxes. Cambridge University Press, 2009, p. 128.

[Kneale1957-2] Kneale, William (1957). "Aristotle and the Consequentia Mirabilis". The Journal of Hellenic Studies. 77 (1): 62–66. doi:10.2307/628635. JSTOR 628635. S2CID 163283107.

[3] Barnes, Jonathan. The Pre-Socratic Philosophers: The Arguments of the Philosophers. Routledge, 1982, p. 217 (p 277 in 1979 edition).

[1]

[2]

[3]