Consistency

In logic , a set of statements is considered consistent or free of contradiction if no contradiction can be derived from it, i.e. no expression and at the same time its negation. Since one could prove anything, even nonsensical, with inconsistent sets of statements, consistency is essential for useful scientific theories , logical calculi, or systems of mathematical axioms .

An additional axiom is said to be relatively consistent with an existing set of statements if its addition does not introduce any new contradictions. In other words: if the set of statements is assumed to be consistent, it is also consistent with the additional axiom.

Furthermore, two additional axioms are said to be equiconsistent with respect to an existing set of statements if the addition of one does not introduce any new contradictions if and only if the other does not either.

Definitions

One always considers a given calculus with a derivability operator , which means something like: from is derivable. ${\displaystyle \vdash }$ ${\displaystyle A\vdash B}$ ${\displaystyle A\,}$ ${\displaystyle B\,}$

The consistency (or freedom from contradictions) is then defined as follows both for a set of formulas and for the entire calculus:

• A formula set is called consistent in the calculus if there is a formula for which does not apply. In words: not everything can be derived from. ${\displaystyle \Gamma \,}$ ${\displaystyle A}$ ${\displaystyle \Gamma \vdash A}$ ${\displaystyle \Gamma }$
• The calculus is called consistent if the empty formula set is consistent in the calculus.
• An inconsistent formula set in the calculus is called inconsistent in the calculus .
• An inconsistent calculus is called inconsistent .
• The formula set is called consistent relative to in the calculus if it follows from the consistency of the formula set that the union of both formula sets is also consistent in the calculus. ${\displaystyle \mathrm {A} \,}$ ${\displaystyle \Gamma \,}$ ${\displaystyle \Gamma \,}$

These definitions are formulated here in general for any calculus. In classical logic and in intuitionistic logic , the consistency can be defined without contradiction in accordance with the name , in that no formula applies to any formula ; This is equivalent here, because from the inconsistency follows the derivability of every formula, thus also all contradictions of the form , and conversely, from every contradiction in these logics follows any formula according to the rule ex contradictione sequitur quodlibet . But there are also logics in which this rule does not apply, so-called paraconsistent logics ; this variant of the definition does not fit them. ${\displaystyle \Gamma \vdash A\land \neg A}$ ${\displaystyle A\,}$ ${\displaystyle A\ \land \neg A}$

In general, the consistency is divided into different levels, depending on which language is given. The weakest is the syntactic consistency ( post- contradiction- free). Analogous to the consistency in the calculus, this requires that there is an expression with , i.e. there is at least one non-derivable expression. If the underlying language has the negation sign (as in classical or intutionist logic), then, as already mentioned, the classical consistency can be formulated: there is an expression for which it applies that not simultaneously and (i.e. ). If there is also semantics, there is semantic consistency (correctness of the calculation): From follows . Finally, it implies the semantic consistency, the classical consistency, and this in turn implies the syntactic consistency. ${\displaystyle A}$ ${\displaystyle \nvdash A}$ ${\displaystyle A}$ ${\displaystyle \vdash A}$ ${\displaystyle \vdash \neg A}$ ${\displaystyle \nvdash A\land \neg A}$ ${\displaystyle \vdash A}$ ${\displaystyle \vDash A}$

The consistency of a calculus can also be shown by a model by proving its semantic correctness .

Evidence of inconsistency

The downside of non-contradiction and consistency is inconsistency, which is usually easy to show because only a single derivation of a contradiction is necessary for this. The most famous simple classical proof of inconsistency is the derivation of Russell's antinomy in Gottlob Frege's arithmetic calculus, which Bertrand Russell discovered in 1902. A more general proof of inconsistency (for classical, intuitionistic and paraconsistent logics) is the derivation of Curry's Paradox 1942, in which the relative inconsistency of a self-referential statement is shown.

A clear example of an inconsistent set of statements can be formulated in the context of traditional syllogistics . The following statements form a contradicting set of statements in the syllogistic calculus, in particular the evident statements (3) (4) in the current present tense are not free of contradictions relative to the evident statements (1) (2) in the historical present :

(1) All people are living beings.

(2) All of Socrates' ancestors are human.

(3) All of Socrates' ancestors are dead.

(4) The dead are not living beings.

The proof of inconsistency is based on three steps:

From (1) and (2) follows (5): All ancestors of Socrates are living beings; The syllogism Barbara was used here .

From (4) and (5) it follows (6): Some ancestors of Socrates are not dead; The syllogism Cesaro was used here .

(6) contradicts (3); The adversarial property was used here.

This proof of inconsistency can be formalized with the usual formulas and initials for the terms used:

Proposition formulas: (1) MaL, (2) VaM, (3) VaT, (4) TeL, (5) VaL, (6) VoT

Formal derivation steps: MaL, VaM VaL (Barbara). TeL, VaL VoT (Cesaro). VaT, VoT VaT VaT (adversarial). ${\displaystyle \vdash }$ ${\displaystyle \vdash }$ ${\displaystyle \vdash }$ ${\displaystyle \land }$ ${\displaystyle \neg }$

Many popular antinomies and paradoxes do not refer to a calculus, but are based on intuitive, opaque, illicit conclusions. It is therefore important to regulate the logical inference in calculi; only then do the inconsistent steps that lead to paradoxes become clearly visible, for example with the liar's paradox .

Proofs of freedom from contradiction

The need for proofs of freedom from contradiction arose at the turn of the 20th century, when contradictions became known in set theory . Georg Cantor , the founder of set theory, discovered it himself and wrote to David Hilbert in 1897 about Cantor's first antinomy . In 1899 Hilbert gave a relative consistency proof of geometry to the arithmetic of real numbers. The following year he asked the question “Are the arithmetic axioms free of contradictions?” As the second of his famous mathematical problems . In 1903 Russell made the problem of consistency in general aware and drafted his type theory from 1903 to 1908 , which was incorporated into the " Principia mathematica " in 1910 . Ernst Zermelo created the axiomatic set theory in 1907 , which later became established in mathematics in the form of the extended Zermelo-Fraenkel set theory ZF or ZFC. No contradictions could be derived from it so far.

However, in order to gain certainty that fundamentally no contradictions can arise, Hilbert developed his program from 1918 to prove the consistency of logic, and outlined methods for proofs of consistency, which are more demanding, since contradictions must be excluded for all possible derivations. His plan became known as Hilbert's program and was successfully implemented for key areas of logic:

• The consistency of classical propositional logic was demonstrated by Paul Bernays in 1918/1926 and by Emil Leon Post in 1921 .
• The consistency of classical first order predicate logic was demonstrated by John von Neumann in 1925 .

Hilbert's program, which was limited to finite metalogical evidence, failed with arithmetic and the axiom systems based on it, as Kurt Gödel showed in his incompleteness theorems of 1930. Subsequent mathematicians therefore modified Hilbert's program by expanding the evidence (e.g. to include transfinite methods) and thus achieved new results:

• The consistency of arithmetic was proven in 1936 by Gerhard Gentzen .
• The consistency of general set theory (without the axiom of infinity ) was demonstrated by Wilhelm Ackermann in 1936, referring to Gentzen.
• The consistency of branched type theory and classical analysis was demonstrated in 1951 by Paul Lorenzen .

Neumann and Zermelo had already tread new paths that deviated from Hilbert's program when they introduced the now established ZF set calculus (Neumann's predecessor of Neumann-Bernays-Gödel set theory ). Within set theory, they created models of set theory and used this for proofs of freedom from contradiction:

• The consistency of the foundation axiom relative to ZF without a foundation axiom was shown in 1929 by John von Neumann using a model
• The consistency of general set theory (ZFC without the axiom of infinity) was shown in 1930 by Ernst Zermelo with a model in ZFC, as was the consistency of ZFC in a meta set theory with strongly unreachable cardinal numbers.

Because of Gödel's incompleteness theorems, however, the consistency of ZF set theory cannot be proven without much stronger meta-axioms. Therefore, within the framework of the usual set theory ZF, the question of their own consistency remains undecidable. Gödel started from her and was thus able to provide relative proof of consistency for controversial additional axioms to ZF:

• The consistency of the axiom of choice and the generalized continuum hypothesis relative to ZF was proven in 1940 by Kurt Gödel.

Web links

Peter H. Starke: Logical Foundations of Computer Science. Lecture notes October 2000

See also

• Theorem of contradiction
• Science - scientific method
• falsification
• ω-consistent theory

Individual evidence

1. ↑ Hilbert / Ackermann: Grundzüge der Theoretischen Logic, Berlin, Heidelberg, 6th edition, 1972, p. 99
2. ↑ Hilbert / Ackermann: Grundzüge der Theoretischen Logic, Berlin, Heidelberg, 1st edition 1928 to 3rd edition 1949, there p. 31
3. ↑ Russell's letter to Frege of June 16, 1902. In: Gottlob Frege: Correspondence with D.Hilbert, E. Husserl, B. Russell , eds. G. Gabriel, F. Kambartel, C. Thiel, Hamburg 1980, pp. 59f limited preview in Google Book search
4. ^ Letter from Cantor to Hilbert dated September 26, 1897, in: Georg Cantor, Briefe, eds. H. Meschkowski and W. Nilson, Berlin, Heidelberg, New York 1999, p. 388
5. ^ David Hilbert: Basics of Geometry , 1st edition, Leipzig 1899th 14th edition, ed. by Michael Toepell, Teubner, Leipzig 1999.
6. ↑ David Hilbert: Mathematical Problems , 1900, in: Archives for Mathematics and Physics, 3rd series, Volume I (1901), pp. 44–63, 213–237
7. ↑ David Hilbert: Axiomatic Thinking , 1918, in: Mathematische Annalen 78 (1918), pp. 405-415
8. ↑ David Hilbert: New Foundation of Mathematics , 1922, in: Treatises from the Mathematical Seminar of the Hamburg University, Volume I (1922), pp. 157–177
9. ↑ David Hilbert: The logical foundations of mathematics , 1922, in: Mathematische Annalen 88 (1923), pp. 151-165
10. ^ Paul Bernays: Axiomatic investigation of the propositional calculus of the "Principia Mathematica" , habilitation thesis Göttingen 1918, abbreviated in: Mathematische Zeitschrift 25 (1926), pp. 305-320
11. ^ Emil Leon Post: Introduction to a General Theory of Elementary Propositions In: American Journal of Mathematics. Volume 43, 1921, pp. 163-185.
12. ^ John von Neumann: On Hilbert's theory of proof , 1925, In: Mathematische Zeitschrift 26 (1927), pp. 1-46
13. ↑ Kurt Gödel: About formally undecidable sentences of the Principia Mathematica and related systems , 1930, In : monthshefte für Mathematik und Physik 38 (1931), S. 173-198
14. ↑ Gerhard Genzten: The consistency of pure number theory In: Mathematische Annalen. 112: 493-565 (1936)
15. ↑ Wilhelm Ackermann: The consistency of general set theory , 1936, In: Mathematische Annalen. 114: 305-315 (1937).
16. ^ Paul Lorenzen: The consistency of classical analysis. In: Mathematical Journal. 54 (1951) pp. 1-24
17. ^ John von Neumann: About a consistency question in axiomatic set theory In: Journal for pure and applied mathematics (Crelle) 160 (1929), pp. 227-241
18. ↑ Ernst Zermelo: limiting numbers and ranges of amounts , in: Fundamenta Mathematicae 16 (1930), pp 29-47
19. ↑ Kurt Gödel: The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory In: Annals of Mathematical Studies. Volume 3, Princeton University Press, Princeton, NJ, 1940, ed. In: Collected Works II, Oxford 1990, pp. 33-101