Доказательство непротиворечивости Генцена - Gentzen's consistency proof

Доказательство непротиворечивости Генцена является результатом теории доказательств в математической логике , опубликованной Генцен в 1936 году показывает , что Пеано аксиом арифметики первого порядка не содержат противоречия (т.е. являются « последовательным »), до тех пор , как некоторые другие Система, использованная в доказательстве, также не содержит противоречий. Эта другая система, называемая сегодня « примитивной рекурсивной арифметикой с дополнительным принципом бескванторной трансфинитной индукции до порядкового числа ε 0 », не является ни слабее, ни сильнее системы аксиом Пеано. Гентцен утверждал, что он избегает сомнительных способов вывода, содержащихся в арифметике Пеано, и поэтому его согласованность менее спорна.

Теорема Генцена

Теорема Генцена касается арифметики первого порядка: теории натуральных чисел , включая их сложение и умножение, аксиоматизированную аксиомами Пеано первого порядка . Это теория «первого порядка»: кванторы распространяются на натуральные числа, но не на множества или функции натуральных чисел. Теория достаточно сильна, чтобы описывать рекурсивно определенные целочисленные функции, такие как возведение в степень, факториалы или последовательность Фибоначчи .

Генцен показал, что непротиворечивость аксиом Пеано первого порядка доказуема над базовой теорией примитивно-рекурсивной арифметики с дополнительным принципом бескванторной трансфинитной индукции до порядкового числа ε 0 . Примитивно-рекурсивная арифметика - это очень упрощенная форма арифметики, которая не вызывает споров. Дополнительный принцип неформально означает, что существует хороший порядок на множестве конечных корневых деревьев . Формально ε 0 - это первый порядковый номер такой, что и является счетным порядковым номером, намного меньшим, чем большие счетные порядковые числа . Это предел последовательности:

Чтобы выразить порядковые числа на языке арифметики, необходима порядковая запись , т. Е. Способ присваивать натуральные числа порядковым числам меньше ε 0 . Это можно сделать по-разному, например, в теореме Кантора о нормальной форме . Для любой бескванторной формулы A (x) нам потребуется: если существует ординал a <ε 0, для которого A (a) ложно, то существует наименьший такой ординал.

Генцен определяет понятие «процедуры редукции» для доказательств в арифметике Пеано. Для данного доказательства такая процедура производит дерево доказательств, причем данное доказательство служит корнем дерева, а другие доказательства в определенном смысле «проще», чем данное. Эта возрастающая простота формализуется путем добавления ординала <ε 0 к каждому доказательству и демонстрации того, что по мере движения вниз по дереву эти порядковые номера становятся меньше с каждым шагом. Затем он показывает, что если бы было доказательство противоречия, процедура редукции привела бы к бесконечной убывающей последовательности ординалов, меньших, чем ε 0, созданной примитивной рекурсивной операцией на доказательствах, соответствующих бескванторной формуле.

Доказательство Генцена можно интерпретировать в терминах теории игр ( Tait 2005 ).

Связь с программой Гильберта и теоремой Гёделя

Доказательство Генцена подчеркивает один часто упускаемый аспект второй теоремы Гёделя о неполноте . Иногда утверждают, что непротиворечивость теории может быть доказана только с помощью более сильной теории. Теория Генцена, полученная добавлением бескванторной трансфинитной индукции к примитивной рекурсивной арифметике, доказывает непротиворечивость арифметики Пеано первого порядка (PA), но не содержит PA. Например, он не доказывает обычную математическую индукцию для всех формул, в отличие от PA (поскольку все примеры индукции являются аксиомами PA). Теория Генцена также не содержится в PA, поскольку она может доказать теоретико-числовой факт - непротиворечивость PA, - чего PA не может. Следовательно, эти две теории в определенном смысле несравнимы .

Тем не менее, есть и другие, более эффективные способы сравнения силы теорий, наиболее важный из которых определяется в терминах понятия интерпретируемости . Можно показать, что если одна теория T интерпретируема в другой B, то T согласована, если B. (На самом деле, это важный момент в понятии интерпретируемости.) И, если предположить, что T не является чрезвычайно слабым, T сам сможет доказать эту самую условность: если B непротиворечив, то и T. Следовательно, T не может докажите, что B непротиворечиво, с помощью второй теоремы о неполноте, тогда как B вполне может быть в состоянии доказать, что T непротиворечиво. Это то, что мотивирует идею использования интерпретируемости для сравнения теорий, т. Е. Мысль о том, что если B интерпретирует T, то B по крайней мере так же силен (в смысле «силы согласованности»), как T.

Сильная форма второй теоремы о неполноте, доказанная Павлом Пудлаком, который основывался на более ранней работе Соломона Фефермана , утверждает, что никакая непротиворечивая теория T, содержащая арифметику Робинсона , Q, не может интерпретировать Q плюс Con (T), утверждение, что T согласуется. В отличие от этого , Q + Con (T) , делает интерпретации T, сильной формой arithmetized теоремы полноты . Таким образом, Q + Con (T) всегда сильнее (в одном хорошем смысле), чем T. Но теория Генцена тривиально интерпретирует Q + Con (PA), поскольку она содержит Q и доказывает Con (PA), и поэтому теория Генцена интерпретирует PA. Но, согласно результату Пудлака, PA не может интерпретировать теорию Генцена, поскольку теория Генцена (как только что было сказано) интерпретирует Q + Con (PA), и интерпретируемость транзитивна. То есть: если PA действительно интерпретировал теорию Генцена, то он также интерпретировал бы Q + Con (PA) и, следовательно, был бы непоследовательным, согласно результату Пудлака. Итак, в смысле силы последовательности, характеризующейся интерпретируемостью, теория Генцена сильнее арифметики Пеано.

Герман Вейль сделал следующий комментарий в 1946 году относительно значения результата Гентцена о неполноте после разрушительного воздействия результата Гёделя 1931 года о неполноте на план Гильберта по доказательству непротиворечивости математики.

Вполне вероятно, что все математики в конечном итоге приняли бы подход Гильберта, если бы он смог успешно его реализовать. Первые шаги были вдохновляющими и многообещающими. Но затем Гёдель нанес ей сокрушительный удар (1931 г.), от которого она еще не оправилась. Гёдель определенным образом перечислил символы, формулы и последовательности формул в формализме Гильберта и таким образом преобразовал утверждение о непротиворечивости в арифметическое предложение. Он смог показать, что это утверждение нельзя ни доказать, ни опровергнуть в рамках формализма. Это может означать только две вещи: либо рассуждение, с помощью которого дается доказательство непротиворечивости, должно содержать некоторый аргумент, который не имеет формального аналога в системе, т. Е. Нам не удалось полностью формализовать процедуру математической индукции; или нужно вообще отказаться от надежды на строго «конечное» доказательство непротиворечивости. Когда Г. Генцену наконец удалось доказать непротиворечивость арифметики, он действительно вышел за эти пределы, провозгласив очевидным тип рассуждения, который проникает во «второй класс порядковых чисел Кантора».

Клини (2009 , с. 479) в 1952 г. сделал следующий комментарий о значении результата Гентцена, особенно в контексте формалистической программы, инициированной Гильбертом.

Первоначальные предложения формалистов обезопасить классическую математику с помощью доказательства непротиворечивости не предполагали использования такого метода, как трансфинитная индукция до ε 0 . В какой степени доказательство Генцена может быть принято как обеспечивающее классическую теорию чисел в смысле этой формулировки проблемы, при нынешнем положении дел является вопросом индивидуального суждения, в зависимости от того, насколько человек готов принять индукцию до ε 0 как конечный результат. метод.

Другие доказательства непротиворечивости арифметики

Первая версия доказательства непротиворечивости Генцена не была опубликована при его жизни, потому что Пол Бернейс возражал против метода, неявно использованного в доказательстве. Модифицированное доказательство, описанное выше, было опубликовано в 1936 году в « Анналах» . Гентцен опубликовал еще два доказательства непротиворечивости, одно в 1938 году, а другое в 1943 году. Все они содержатся в ( Gentzen & Szabo 1969 ).

В 1940 году Вильгельм Акерманн опубликовал еще одно доказательство непротиворечивости арифметики Пеано, также использующее порядковый номер ε 0 .

Работа, начатая доказательством Генцена

Доказательство Генцена - это первый пример того, что называется порядковым анализом теоретико-доказательной базы . В ординальном анализе сила теорий оценивается путем измерения того, насколько велики (конструктивные) ординалы, которые могут быть доказаны как хорошо упорядоченные, или, что эквивалентно, насколько велик (конструктивный) ординал может быть доказан трансфинитной индукцией. Конструктивный ординал - это тип порядка рекурсивного упорядочивания натуральных чисел.

Лоуренс Кирби и Джефф Пэрис доказали в 1982 году, что теорема Гудштейна не может быть доказана в арифметике Пеано. Их доказательство было основано на теореме Генцена.

Заметки

Рекомендации