Введение
Концепция математической логики. Доказательство непротиворечивости Гентцена — это результат теории доказательств в математической логике, опубликованный Герхардом Гентценом в 1936 году. Оно показывает, что аксиомы Пеано арифметики первого порядка не содержат противоречий (то есть являются "непротиворечивыми"), при условии, что другая система, используемая в доказательстве, также не содержит противоречий. Эта другая система, которую сегодня называют "примитивно рекурсивной арифметикой с дополнительным принципом трансфинитной индукции без кванторов до ординала ε0", не слабее и не сильнее системы аксиом Пеано. Гентцен утверждал, что она избегает сомнительных правил вывода, содержащихся в арифметике Пеано, и поэтому её непротиворечивость вызывает меньше споров.
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.
Теорема Гентцена
Теорема Гентцена относится к арифметике первого порядка: теории натуральных чисел, включающей сложение и умножение, аксиоматизированной аксиомами Пеано первого порядка. Это теория "первого порядка": кванторы простираются на натуральные числа, но не на множества или функции натуральных чисел. Теория достаточно мощна, чтобы описать рекурсивно определенные целочисленные функции, такие как возведение в степень, факториалы или последовательность Фибоначчи. Гентцен показал, что непротиворечивость аксиом Пеано первого порядка доказуема относительно базовой теории примитивно рекурсивной арифметики с дополнительным принципом кванторно-свободной трансфинитной индукции до ординала ε0. Примитивно рекурсивная арифметика – это значительно упрощенная форма арифметики, которая не вызывает особых споров. Дополнительный принцип означает, неформально, что существует хорошее упорядочение на множестве конечных корневых деревьев. Формально, ε0 – это первый ординал такой, что , то есть предел последовательности. Это счетный ординал, значительно меньший, чем большие счетные ординалы. Для выражения ординалов на языке арифметики необходима ординальная нотация, то есть способ присвоения натуральных чисел ординалам, меньшим ε0. Это можно сделать различными способами, одним из примеров является теорема о нормальной форме Кантора. Доказательство Гентцена основано на следующем предположении: для любой кванторно-свободной формулы A(x), если существует ординал a < ε0, для которого A(a) ложно, то существует наименьший такой ординал. Гентцен определяет понятие "процедуры редукции" для доказательств в арифметике Пеано. Для заданного доказательства такая процедура порождает дерево доказательств, где данное служит корнем дерева, а остальные доказательства в некотором смысле "проще" исходного. Эта возрастающая простота формализуется путем прикрепления к каждому доказательству ординала < ε0 и показа того, что при движении вниз по дереву эти ординалы уменьшаются на каждом шаге. Затем он показывает, что если бы существовало доказательство противоречия, процедура редукции привела бы к бесконечной строго убывающей последовательности ординалов, меньших ε0, порожденной примитивно рекурсивной операцией над доказательствами, соответствующими кванторно-свободной формуле.
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.
Другие доказательства последовательности арифметических вычислений
Первая версия доказательства непротиворечивости Гентцена не была опубликована при его жизни, поскольку Пол Бернайс возражал против метода, неявно использованного в доказательстве. Модифицированное доказательство, описанное выше, было опубликовано в 1936 году в "Анналах". Гентцен впоследствии опубликовал еще два доказательства непротиворечивости, одно в 1938 году и одно в 1943 году. Все они содержатся в работах, где Курт Гёдель переинтерпретировал доказательство Гентцена 1936 года в лекции 1938 года, что получило название интерпретации "без контрпримеров". И исходное доказательство, и его переформулировка могут быть поняты в терминах теории игр. В 1940 году Вильгельм Аккерман опубликовал еще одно доказательство непротиворечивости арифметики Пеано, также используя ординал ε0. Другое доказательство непротиворечивости арифметики было опубликовано И. Н. Хлодовским в 1959 году. Дополнительные доказательства непротиворечивости арифметики были опубликованы: Т. Дж. Степинем и Л. Т. Степинем (в 2018 году) и С. Артемовым (в 2019 году). В статье Степиней утверждается, что доказательство непротиворечивости (опубликованное там) арифметической системы выполняется внутри этой системы. В статье Артемова заявлено, что доказательство, опубликованное там, формализуемо в арифметике Пеано.
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.
Работа, начатая доказательством Гентцена
Доказательство Гентцена — это первый пример того, что называется доказательно-теоретическим порядковым анализом. В порядковом анализе оценивают силу теорий, измеряя, насколько велики (конструктивные) ординалы, которые можно доказать как хорошо упорядоченные, или, что эквивалентно, для какого (конструктивного) ординала можно доказать трансфинитную индукцию. Конструктивный ординал — это тип упорядочения рекурсивного хорошего упорядочения натуральных чисел. В этих терминах работа Гентцена устанавливает, что доказательно-теоретический ординал арифметики Пеано первого порядка равен ε0. Лоуренс Кирби и Джефф Пэрис доказали в 1982 году, что теорему Гудштейна нельзя доказать в арифметике Пеано. Их доказательство основывалось на теореме Гентцена.