Доказательство согласованности Gentzens - Gentzens consistency proof - Wikipedia

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

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

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

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

{ displaystyle omega, omega ^ { omega}, omega ^ { omega ^ { omega}}, ldots}

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

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

Доказательство Генцена можно интерпретировать в терминах теории игр (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.

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

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

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

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

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

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

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

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

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

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

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

Примечания

^ Видеть Клини (2009), pp. 476–499) для полного изложения доказательства Генцена и различных комментариев по историческому и философскому значению результата.
^ Пудлак, Павел (01.06.1985). «Сокращения, заявления о согласованности и интерпретации». Журнал символической логики. 50 (2): 423–441. Дои:10.2307/2274231. ISSN 0022-4812. JSTOR 2274231.
^ Феферман, С. «Арифметизация метаматематики в общем контексте». Fundamenta Mathematicae. 49 (1). ISSN 0016-2736.
^ Вейль (2012, п. 144).