Гентценнің тұрақтылық дәлелі және Пеано аксиомалары

Mathematical logic concept
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.

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.

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
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. 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. Yet other proofs of consistency of Arithmetic were published by: T. J. Stępień and Ł. T. Stępień (in 2018) and by S. Artemov (in 2019). In the Stępieńs' paper it has been claimed that the proof of consistency (published there), of the Arithmetic System, is done within this System. In Artemov's paper it has been stated that the proof published there, is formalizable in Peano Arithmetic.

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.