Philosophy: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:
- [math]\displaystyle{ (\neg A \to A) \to A }[/math].
Derivations
Intuitionistic logic
The principle of non-contradiction is equivalent to [math]\displaystyle{ \neg\big((\neg A\to A)\land\neg A\big) }[/math], which in turn is equivalent to
- [math]\displaystyle{ (\neg A\to A) \to \neg \neg A }[/math]
This result can also be seen as the special case of
- [math]\displaystyle{ \big((A\to B)\to A\big) \to \big((A\to B)\to B\big) }[/math]
for [math]\displaystyle{ B=\bot }[/math]. This proposition follows from the propositional form of modus ponens [math]\displaystyle{ A \to \big((A\to B)\to B\big) }[/math] together with the fact that always [math]\displaystyle{ A \to (C\to B)\vdash(C\to A) \to (C\to B) }[/math].
Since [math]\displaystyle{ D \to \neg \neg A }[/math] is always also intuitionistically equivalent to [math]\displaystyle{ \neg \neg (D \to A) }[/math], the above also constructively establishes the double negation of consequentia mirabilis.
Classical logic
Consequentia mirabilis follows from the above by double-negation elimination.
Indeed, the result is also established when using the classically valid propositional form of the reverse disjunctive syllogism [math]\displaystyle{ (B\to A)\to (\neg B\lor A) }[/math] with the double-negation elimination principle in the form [math]\displaystyle{ (\neg \neg A \lor A) \to A }[/math].
Related to the second intuitionistic derivation given above, consequentia mirabilis also follow as the special case of Pierce's law
- [math]\displaystyle{ \big((A\to B)\to A\big) \to A }[/math]
for [math]\displaystyle{ B=\bot }[/math].
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."[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]
See also
- Ex falso quodlibet
- Tertium non datur
- Peirce's law
References
- ↑ 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.
- ↑ Barnes, Jonathan. The Pre-Socratic Philosophers: The Arguments of the Philosophers. Routledge, 1982, p. 217 (p 277 in 1979 edition).
 |  |
