Consequentia mirabilis

Last updated

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:

Contents

.

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

Minimal logic

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

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 , it follows that

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

Consequentia mirabilis thus holds whenever . 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 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 principle is equivalent to . The claim now follows from , i.e. the fact that there are equivalent characterizations of two propositions being mutually exclusive.

So minimal logic validates that holds exactly when it is implied by both and .

Equivalence to excluded middle

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 and each imply , and either of them must hold, then follows. Formally,

For and , the principle of identity now entails

Intuitionistic logic

One has that implies . By conjunction elimination, this is in fact an equivalence. In particular, one has

The right hand of this also implies , 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 . This holds because the principle of explosion itself may be formulated as .

Classical logic

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 chained together with the double-negation elimination principle in the form .

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

for . That article can be consulted for more, related equivalences.

See also

Related Research Articles

<span class="mw-page-title-main">Logical connective</span> Symbol connecting sentential formulas in logic

In logic, a logical connective is a logical constant. Connectives can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary connective can be used to join the two atomic formulas and , rendering the complex formula .

<span class="mw-page-title-main">De Morgan's laws</span> Pair of logical equivalences

In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathematician. The rules allow the expression of conjunctions and disjunctions purely in terms of each other via negation.

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

<span class="mw-page-title-main">Contradiction</span> Logical incompatibility between two or more propositions

In traditional logic, a contradiction occurs when a proposition conflicts either with itself or established fact. It is often used as a tool to detect disingenuous beliefs and bias. Illustrating a general tendency in applied logic, Aristotle's law of noncontradiction states that "It is impossible that the same thing can at the same time both belong and not belong to the same object and in the same respect."

<span class="mw-page-title-main">Negation</span> Logical operation

In logic, negation, also called the logical not or logical complement, is an operation that takes a proposition to another proposition "not ", standing for " is not true", written , or . It is interpreted intuitively as being true when is false, and false when is true. Negation is thus a unary logical connective. It may be applied as an operation on notions, propositions, truth values, or semantic values more generally. In classical logic, negation is normally identified with the truth function that takes truth to falsity. In intuitionistic logic, according to the Brouwer–Heyting–Kolmogorov interpretation, the negation of a proposition is the proposition whose proofs are the refutations of .

Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.

<span class="mw-page-title-main">Logical biconditional</span> Concept in logic and mathematics

In logic and mathematics, the logical biconditional, also known as material biconditional or equivalence or biimplication or bientailment, is the logical connective used to conjoin two statements and to form the statement " if and only if ", where is known as the antecedent, and the consequent.

In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics.

In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition A is logically equivalent to not (not-A), or by the formula A ≡ ~(~A) where the sign ≡ expresses logical equivalence and the sign ~ expresses negation.

In logic, a truth function is a function that accepts truth values as input and produces a unique truth value as output. In other words: the input and output of a truth function are all truth values; a truth function will always output exactly one truth value, and inputting the same truth value(s) will always output the same truth value. The typical example is in propositional logic, wherein a compound statement is constructed using individual statements connected by logical connectives; if the truth value of the compound statement is entirely determined by the truth value(s) of the constituent statement(s), the compound statement is called a truth function, and any logical connectives used are said to be truth functional.

In mathematical logic, a superintuitionistic logic is a propositional logic extending intuitionistic logic. Classical logic is the strongest consistent superintuitionistic logic; thus, consistent superintuitionistic logics are called intermediate logics.

In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.

In logic, a functionally complete set of logical connectives or Boolean operators is one that can be used to express all possible truth tables by combining members of the set into a Boolean expression. A well-known complete set of connectives is { AND, NOT }. Each of the singleton sets { NAND } and { NOR } is functionally complete. However, the set { AND, OR } is incomplete, due to its inability to express NOT.

In mathematics, a set is inhabited if there exists an element .

In logic and mathematics, contraposition refers to the inference of going from a conditional statement into its logically equivalent contrapositive, and an associated proof method known as proof by contraposition. The contrapositive of a statement has its antecedent and consequent inverted and flipped.

In mathematics and philosophy, Łukasiewicz logic is a non-classical, many-valued logic. It was originally defined in the early 20th century by Jan Łukasiewicz as a three-valued modal logic; it was later generalized to n-valued as well as infinitely-many-valued (0-valued) variants, both propositional and first order. The ℵ0-valued version was published in 1930 by Łukasiewicz and Alfred Tarski; consequently it is sometimes called the Łukasiewicz–Tarski logic. It belongs to the classes of t-norm fuzzy logics and substructural logics.

In constructive mathematics, pseudo-order is a name given to certain binary relations appropriate for modeling continuous orderings.

Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson. It is an intuitionistic and paraconsistent logic, that rejects both the law of the excluded middle as well as the principle of explosion, and therefore holding neither of the following two derivations as valid:

<span class="mw-page-title-main">Peirce's law</span> Axiom used in logic and philosophy

In logic, Peirce's law is named after the philosopher and logician Charles Sanders Peirce. It was taken as an axiom in his first axiomatisation of propositional logic. It can be thought of as the law of excluded middle written in a form that involves only one sort of connective, namely implication.

References

  1. Sainsbury, Richard. Paradoxes. Cambridge University Press, 2009, p. 128.
  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).