Gentzen's consistency proof

Last updated

Gentzen's consistency proof is a result of proof theory in mathematical logic, published by Gerhard Gentzen in 1936. It shows that the Peano axioms of first-order arithmetic do not contain a contradiction (i.e. are "consistent"), as long as a certain other system used in the proof does not contain any contradictions either. This other system, today called "primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal ε0", is neither weaker nor stronger than the system of Peano axioms. Gentzen argued that it avoids the questionable modes of inference contained in Peano arithmetic and that its consistency is therefore less controversial.

Contents

Gentzen's theorem

Gentzen's theorem is concerned with first-order arithmetic: the theory of the natural numbers, including their addition and multiplication, axiomatized by the first-order Peano axioms. This is a "first-order" theory: the quantifiers extend over natural numbers, but not over sets or functions of natural numbers. The theory is strong enough to describe recursively defined integer functions such as exponentiation, factorials or the Fibonacci sequence.

Gentzen showed that the consistency of the first-order Peano axioms is provable over the base theory of primitive recursive arithmetic with the additional principle of quantifier-free transfinite induction up to the ordinal ε0. Primitive recursive arithmetic is a much simplified form of arithmetic that is rather uncontroversial. The additional principle means, informally, that there is a well-ordering on the set of finite rooted trees. Formally, ε0 is the first ordinal such that , i.e. the limit of the sequence

It is a countable ordinal much smaller than large countable ordinals. To express ordinals in the language of arithmetic, an ordinal notation is needed, i.e. a way to assign natural numbers to ordinals less than ε0. This can be done in various ways, one example provided by Cantor's normal form theorem. Gentzen's proof is based on the following assumption: for any quantifier-free formula A(x), if there is an ordinal a< ε0 for which A(a) is false, then there is a least such ordinal.

Gentzen defines a notion of "reduction procedure" for proofs in Peano arithmetic. For a given proof, such a procedure produces a tree of proofs, with the given one serving as the root of the tree, and the other proofs being, in a sense, "simpler" than the given one. This increasing simplicity is formalized by attaching an ordinal < ε0 to every proof, and showing that, as one moves down the tree, these ordinals get smaller with every step. He then shows that if there were a proof of a contradiction, the reduction procedure would result in an infinite strictly descending sequence of ordinals smaller than ε0 produced by a primitive recursive operation on proofs corresponding to a quantifier-free formula. [1]

Relation to Hilbert's program and Gödel's theorem

Gentzen's proof highlights one commonly missed aspect of Gödel's second incompleteness theorem. It is sometimes claimed that the consistency of a theory can only be proved in a stronger theory. Gentzen's theory obtained by adding quantifier-free transfinite induction to primitive recursive arithmetic proves the consistency of first-order Peano arithmetic (PA) but does not contain PA. For example, it does not prove ordinary mathematical induction for all formulae, whereas PA does (since all instances of induction are axioms of PA). Gentzen's theory is not contained in PA, either, however, since it can prove a number-theoretical fact—the consistency of PA—that PA cannot. Therefore, the two theories are, in one sense, incomparable.

That said, there are other, finer ways to compare the strength of theories, the most important of which is defined in terms of the notion of interpretability. It can be shown that, if one theory T is interpretable in another B, then T is consistent if B is. (Indeed, this is a large point of the notion of interpretability.) And, assuming that T is not extremely weak, T itself will be able to prove this very conditional: If B is consistent, then so is T. Hence, T cannot prove that B is consistent, by the second incompleteness theorem, whereas B may well be able to prove that T is consistent. This is what motivates the idea of using interpretability to compare theories, i.e., the thought that, if B interprets T, then B is at least as strong (in the sense of 'consistency strength') as T is.

A strong form of the second incompleteness theorem, proved by Pavel Pudlák, [2] who was building on earlier work by Solomon Feferman, [3] states that no consistent theory T that contains Robinson arithmetic, Q, can interpret Q plus Con(T), the statement that T is consistent. By contrast, Q+Con(T) does interpret T, by a strong form of the arithmetized completeness theorem. So Q+Con(T) is always stronger (in one good sense) than T is. But Gentzen's theory trivially interprets Q+Con(PA), since it contains Q and proves Con(PA), and so Gentzen's theory interprets PA. But, by Pudlák's result, PA cannot interpret Gentzen's theory, since Gentzen's theory (as just said) interprets Q+Con(PA), and interpretability is transitive. That is: If PA did interpret Gentzen's theory, then it would also interpret Q+Con(PA) and so would be inconsistent, by Pudlák's result. So, in the sense of consistency strength, as characterized by interpretability, Gentzen's theory is stronger than Peano arithmetic.

Hermann Weyl made the following comment in 1946 regarding the significance of Gentzen's consistency result following the devastating impact of Gödel's 1931 incompleteness result on Hilbert's plan to prove the consistency of mathematics. [4]

It is likely that all mathematicians ultimately would have accepted Hilbert's approach had he been able to carry it out successfully. The first steps were inspiring and promising. But then Gödel dealt it a terrific blow (1931), from which it has not yet recovered. Gödel enumerated the symbols, formulas, and sequences of formulas in Hilbert's formalism in a certain way, and thus transformed the assertion of consistency into an arithmetic proposition. He could show that this proposition can neither be proved nor disproved within the formalism. This can mean only two things: either the reasoning by which a proof of consistency is given must contain some argument that has no formal counterpart within the system, i.e., we have not succeeded in completely formalizing the procedure of mathematical induction; or hope for a strictly "finitistic" proof of consistency must be given up altogether. When G. Gentzen finally succeeded in proving the consistency of arithmetic he trespassed those limits indeed by claiming as evident a type of reasoning that penetrates into Cantor's "second class of ordinal numbers."

Kleene (2009 , p. 479) made the following comment in 1952 on the significance of Gentzen's result, particularly in the context of the formalist program which was initiated by Hilbert.

The original proposals of the formalists to make classical mathematics secure by a consistency proof did not contemplate that such a method as transfinite induction up to ε0 would have to be used. To what extent the Gentzen proof can be accepted as securing classical number theory in the sense of that problem formulation is in the present state of affairs a matter for individual judgement, depending on how ready one is to accept induction up to ε0 as a finitary method.

In contrast, Bernays (1967) commented on whether Hilbert's confinement to finitary methods was too restrictive:

It thus became apparent that the 'finite Standpunkt' is not the only alternative to classical ways of reasoning and is not necessarily implied by the idea of proof theory. An enlarging of the methods of proof theory was therefore suggested: instead of a reduction to finitist methods of reasoning, it was required only that the arguments be of a constructive character, allowing us to deal with more general forms of inference.

Other consistency proofs of arithmetic

Gentzen's first version of his consistency proof was not published during his lifetime because Paul Bernays had objected to a method implicitly used in the proof. The modified proof, described above, was published in 1936 in the Annals . Gentzen went on to publish two more consistency proofs, one in 1938 and one in 1943. All of these are contained in ( Gentzen & Szabo 1969 ).

Kurt Gödel reinterpreted Gentzen's 1936 proof in a lecture in 1938 in what came to be known as the no-counterexample interpretation. Both the original proof and the reformulation can be understood in game-theoretic terms. ( Tait 2005 ).

In 1940 Wilhelm Ackermann published another consistency proof for Peano arithmetic, also using the ordinal ε0.

Another proof of consistency of Arithmetic was published by I. N. Khlodovskii, in 1959.

Work initiated by Gentzen's proof

Gentzen's proof is the first example of what is called proof-theoretic ordinal analysis. In ordinal analysis one gauges the strength of theories by measuring how large the (constructive) ordinals are that can be proven to be well-ordered, or equivalently for how large a (constructive) ordinal can transfinite induction be proven. A constructive ordinal is the order type of a recursive well-ordering of natural numbers.

In this language, Gentzen's work establishes that the proof-theoretic ordinal of first-order Peano arithmetic is ε0.

Laurence Kirby and Jeff Paris proved in 1982 that Goodstein's theorem cannot be proven in Peano arithmetic. Their proof was based on Gentzen's theorem.

Notes

  1. See Kleene (2009 , pp. 476–499) for a full presentation of Gentzen's proof and various comments on the historic and philosophical significance of the result.
  2. Pudlák 1985.
  3. Feferman 1960.
  4. Weyl (2012 , p. 144).

Related Research Articles

<span class="mw-page-title-main">Gödel's completeness theorem</span> Fundamental theorem in mathematical logic

Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.

In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giuseppe Peano. These axioms have been used nearly unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete.

Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of provability in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.

In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if it has a model, i.e., there exists an interpretation under which all formulas in the theory are true. This is the sense used in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead. The syntactic definition states a theory is consistent if there is no formula such that both and its negation are elements of the set of consequences of . Let be a set of closed sentences and the set of closed sentences provable from under some formal deductive system. The set of axioms is consistent when there is no formula such that and .

In mathematical logic, Goodstein's theorem is a statement about the natural numbers, proved by Reuben Goodstein in 1944, which states that every Goodstein sequence eventually terminates at 0. Laurence Kirby and Jeff Paris showed that it is unprovable in Peano arithmetic. This was the third example of a true statement about natural numbers that is unprovable in Peano arithmetic, after the examples provided by Gödel's incompleteness theorem and Gerhard Gentzen's 1943 direct proof of the unprovability of ε0-induction in Peano arithmetic. The Paris–Harrington theorem gave another example.

In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that arithmetic is consistent – free of any internal contradictions. Hilbert stated that the axioms he considered for arithmetic were the ones given in Hilbert (1900), which include a second order completeness axiom.

Proof theory is a major branch of mathematical logic and theoretical computer science within which proofs are treated as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of a given logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of deriving theorems from axioms. It can be conceptualized as sculpting out necessary conditions from sufficient ones.

In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early 1920s, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies. As a solution, Hilbert proposed to ground all existing theories to a finite, complete set of axioms, and provide a proof that these axioms were consistent. Hilbert proposed that the consistency of more complicated systems, such as real analysis, could be proven in terms of simpler systems. Ultimately, the consistency of all of mathematics could be reduced to basic arithmetic.

In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by Raphael M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is weaker than PA but it has the same language, and both theories are incomplete. Q is important and interesting because it is a finitely axiomatized fragment of PA that is recursively incompletable and essentially undecidable.

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 mathematics, the epsilon numbers are a collection of transfinite numbers whose defining property is that they are fixed points of an exponential map. Consequently, they are not reachable from 0 via a finite series of applications of the chosen exponential map and of "weaker" operations like addition and multiplication. The original epsilon numbers were introduced by Georg Cantor in the context of ordinal arithmetic; they are the ordinal numbers ε that satisfy the equation

In mathematical logic, an ω-consistenttheory is a theory that is not only (syntactically) consistent, but also avoids proving certain infinite combinations of sentences that are intuitively contradictory. The name is due to Kurt Gödel, who introduced the concept in the course of proving the incompleteness theorem.

In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and non-circularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of relevance to proof theory still have computable ordinal notations. However, it is not possible to decide effectively whether a given putative ordinal notation is a notation or not ; various more-concrete ways of defining ordinals that definitely have notations are available.

Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician Skolem (1923), as a formalization of his finitistic conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitistic. Many also believe that all of finitism is captured by PRA, but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε0, which is the proof-theoretic ordinal of Peano arithmetic. PRA's proof theoretic ordinal is ωω, where ω is the smallest transfinite ordinal. PRA is sometimes called Skolem arithmetic, although that has another meaning, see Skolem arithmetic.

In proof theory, a discipline within mathematical logic, double-negation translation, sometimes called negative translation, is a general approach for embedding classical logic into intuitionistic logic. Typically it is done by translating formulas to formulas that are classically equivalent but intuitionistically inequivalent. Particular instances of double-negation translations include Glivenko's translation for propositional logic, and the Gödel–Gentzen translation and Kuroda's translation for first-order logic.

In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.

In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic logic into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to provide a consistency proof of arithmetic. The name of the interpretation comes from the journal Dialectica, where Gödel's paper was published in a 1958 special issue dedicated to Paul Bernays on his 70th birthday.

References