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

Концепция математической логики

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

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

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

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

${\displaystyle \omega ,\ \omega ^{\omega },\ \omega ^{\omega ^{\omega }},\ \ldots }$

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

Генцен определяет понятие «процедуры редукции» для доказательств в арифметике Пеано. Для данного доказательства такая процедура создает дерево доказательств, причем данное служит корнем дерева, а другие доказательства, в некотором смысле, «проще» данного. Эта возрастающая простота формализуется путем присоединения ординала < ε ₀ к каждому доказательству и показа того, что по мере продвижения вниз по дереву эти ординалы становятся меньше с каждым шагом. Затем он показывает, что если бы существовало доказательство противоречия, процедура редукции привела бы к бесконечной строго убывающей последовательности ординалов, меньших ε _{0 ,} произведенной примитивной рекурсивной операцией над доказательствами, соответствующими формуле без кванторов. ^[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), от которого он до сих пор не оправился. Гёдель определенным образом перечислил символы, формулы и последовательности формул в формализме Гильберта и таким образом преобразовал утверждение о непротиворечивости в арифметическое предложение. Он смог показать, что это предложение не может быть ни доказано, ни опровергнуто в рамках формализма. Это может означать только две вещи: либо рассуждение, с помощью которого дается доказательство непротиворечивости, должно содержать некоторый аргумент, не имеющий формального аналога в системе, т. е. нам не удалось полностью формализовать процедуру математической индукции; либо надежда на строго «финитное» доказательство непротиворечивости должна быть полностью оставлена. Когда Г. Генцену наконец удалось доказать непротиворечивость арифметики, он действительно перешел эти границы, заявив, что очевиден тип рассуждения, который проникает во «второй класс порядковых чисел» Кантора.

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

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

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

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

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

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

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

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

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

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

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

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

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

Примечания

1. Полное изложение доказательства Генцена и различные комментарии об историческом и философском значении результата см. в книге Клини (2009, стр. 476–499).
2. Пудлак 1985.
3. Феферман 1960.
4. Вейль (2012, стр. 144).

Ссылки

• Эдвардс, Пол, ред. (1967). «Пол Бернайс». Энциклопедия философии . Том 3. MacMillan and Free Press. стр. 502.
• Феферман, Соломон (1960). «Арифметизация метаматематики в общей постановке». Fundamenta Mathematicae . 49 (1): 35–92. doi : 10.4064/fm-49-1-35-92 . ISSN  0016-2736.
• Генцен, Герхард (1936), «Die Widerspruchsfreiheit der Reinen Zahlentheorie», Mathematische Annalen , 112 : 493–565, doi : 10.1007/BF01565428, S2CID  122719892– Переведено как «Последовательность арифметики» в (Gentzen & Szabo 1969).
• Генцен, Герхард (1938), «Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie», Forschungen zur Logik und zur Grundlegung der Exakten Wissenschaften , 4 : 19–44– Переведено как «Новая версия доказательства непротиворечивости для элементарной теории чисел» в (Gentzen & Szabo 1969).
• Генцен, Герхард (1969), Сабо, М.Э. (ред.), Сборник статей Герхарда Генцена , Исследования по логике и основаниям математики (издание в твердом переплете), Амстердам: Северная Голландия, ISBN 978-0-7204-2254-2- перевод статей на английский язык.
• Гёдель, К. (2001) [1938], «Лекция у Цильзеля», в Феферман, Соломон (ред.), Курт Гёдель: Собрание сочинений , т. III Неопубликованные эссе и лекции (мягкая обложка), Oxford University Press Inc., стр. 87–113, ISBN 978-0-19-514722-3
• Джервелл, Герман Руге (1999), Курс теории доказательств (черновик учебника), архивировано из оригинала 2011-06-07
• Хлодовский, И.Н. (1959), «Новое доказательство непротиворечивости арифметики» (PDF) , Успехи Матем. Наук , 14 (6(90)): 105–140
• Kirby, L.; Paris, J. (1982), "Доступные результаты независимости для арифметики Пеано" (PDF) , Bull. London Math. Soc. , 14 (4): 285–293, CiteSeerX  10.1.1.107.3303 , doi :10.1112/blms/14.4.285, архивировано из оригинала (PDF) 2014-09-12
• Клини, Стивен Коул (2009) [1952]. Введение в метаматематику . Ishi Press International. ISBN 978-0-923891-57-2.
• Пудлак, Павел (1 июня 1985 г.). «Сокращения, утверждения о согласованности и интерпретации». Журнал символической логики . 50 (2): 423–441. doi :10.2307/2274231. ISSN  0022-4812. JSTOR  2274231.
• Tait, WW (2005), «Переформулировка Гёделем первого доказательства непротиворечивости Генцена для арифметики: интерпретация без контрпримеров» (PDF) , The Bulletin of Symbolic Logic , 11 (2): 225–238, doi :10.2178/bsl/1120231632, ISSN  1079-8986, S2CID  9481361
• Вейль, Герман (2012). Уровни бесконечности: Избранные труды по математике и философии. Нью-Йорк: Dover Publications. ISBN 978-0-486-48903-2.