Доказательство непротиворечивости Генцена

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

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

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

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

\omega ,\ \omega ^{\omega },\ \omega ^{\omega ^{\omega }},\ \ldots

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

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

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

Доказательство Генцена подчеркивает один часто упускаемый из виду аспект второй теоремы Гёделя о неполноте . Иногда утверждают, что непротиворечивость теории можно доказать только с помощью более сильной теории. Теория Генцена, полученная путем добавления бескванторной трансфинитной индукции к примитивно-рекурсивной арифметике, доказывает непротиворечивость арифметики Пеано первого порядка (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) интерпретирует 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 году сделала следующий комментарий о значении результата Генцена, особенно в контексте формалистической программы, инициированной Гильбертом.

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

Напротив, Бернейс (1967) прокомментировал, было ли ограничение Гильберта финитными методами слишком ограничительным:

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

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

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

Курт Гёдель переосмыслил доказательство Генцена 1936 года в лекции 1938 года, так называемую интерпретацию без контрпримеров. И исходное доказательство, и переформулировку можно понять в терминах теории игр. ( Тейт 2005 ).

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

Другое доказательство непротиворечивости арифметики было опубликовано И. Н. Хлодовским в 1959 году.

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

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

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

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

Примечания

↑ См. Kleene (2009 , стр. 476–499) для полного представления доказательства Генцена и различных комментариев об историческом и философском значении результата.
^ Пудели 1985 .
^ Феферман 1960 .
^ Вейль (2012 , стр. 144).

Ссылки

Эдвардс, Пол, изд. (1967). «Пол Бернейс». Энциклопедия философии . Том. 3. Макмиллан и свободная пресса. п. 502.
Феферман, Соломон (1960). «Арифметизация метаматематики в общей постановке» . Фундамента Математика . 49 (1): 35–92. дои : 10.4064/fm-49-1-35-92 . ISSN 0016-2736 .
Генцен, Герхард (1936), «Непротиворечивость чистой теории чисел» , Mathematical Annals , 112 : 493–565, doi : 10.1007/BF01565428 , S2CID 122719892 - Переведено как «Непротиворечивость арифметики», в ( Gentzen & Szabo 1969 ). .
Генцен, Герхард (1938), «Новая версия доказательства непротиворечивости для чистой теории чисел», Research on Logic and Foundation of the Exact Sciences , 4 : 19–44 – Переведено как «Новая версия доказательства непротиворечивости для элементарной теории чисел». ", в ( Гентцен и Сабо, 1969 ).
Генцен, Герхард (1969), Сабо, М.Э. (редактор), Сборник статей Герхарда Генцена , Исследования по логике и основам математики (изд. в твердом переплете), Амстердам: Северная Голландия, ISBN 978-0-7204-2254-2 - английский перевод документов.
Гёдель, К. (2001) [1938], «Лекция у Зильзеля» , в Феферман, Соломон (редактор), Курт Гёдель: Собрание сочинений , том. III Неопубликованные эссе и лекции (изд. в мягкой обложке), Oxford University Press Inc., стр. 87–113, ISBN 978-0-19-514722-3
Джервелл, Герман Руге (1999), Курс теории доказательств (проект учебника), заархивировано из оригинала 7 июня 2011 г.
Хлодовский И. Н. (1959), "Новое доказательство непротиворечивости арифметики" (PDF) , Успехи матем. Наук , 14 (6(90)): 105–140
Кирби, Л .; Пэрис, Дж. (1982), «Доступные результаты независимости для арифметики Пеано» (PDF) , Bull. Лондонская математика. Соц. , 14 (4): 285–293, CiteSeerX 10.1.1.107.3303 , doi : 10.1112/blms/14.4.285 , заархивировано из оригинала (PDF) 12 сентября 2014 г.
Клини, Стивен Коул (2009) [1952]. Введение в метаматематику . Иши Пресс Интернешнл. ISBN 978-0-923891-57-2 .
Пудлак, Павел (1 июня 1985 г.). «Сокращения, заявления о непротиворечивости и интерпретации» . Журнал символической логики . 50 (2): 423–441. дои : 10.2307/2274231 . ISSN 0022-4812 . JSTOR 2274231 .
Тейт, WW (2005), «Переформулировка Гёделя первого доказательства непротиворечивости арифметики Генцена: интерпретация без контрпримеров» (PDF) , The Bulletin of Символическая логика , 11 (2): 225–238, doi : 10.2178/bsl/1120231632 , ISSN 1079-8986 , S2CID 9481361
Вейль, Герман (2012). Уровни бесконечности: Избранные сочинения по математике и философии . Нью-Йорк: Dover Publications. ISBN 978-0-486-48903-2 .

[1] См. Kleene (2009 , стр. 476–499) для полного представления доказательства Генцена и различных комментариев об историческом и философском значении результата.

[FOOTNOTEPudlák1985-2] Пудели 1985 .

[FOOTNOTEFeferman1960-3] Феферман 1960 .

[4] Вейль (2012 , стр. 144).

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]