В математике вторая проблема Гильберта была поставлена Давидом Гильбертом в 1900 году как одна из его 23 проблем . Она требует доказательства того, что арифметика непротиворечива – свободна от каких-либо внутренних противоречий. Гильберт заявил, что аксиомы, которые он рассматривал для арифметики, были теми, что даны в Гильберте (1900), которые включают аксиому полноты второго порядка.
В 1930-х годах Курт Гёдель и Герхард Генцен доказали результаты, которые пролили новый свет на проблему. Некоторые считают, что теоремы Гёделя дают отрицательное решение проблемы, в то время как другие рассматривают доказательство Генцена как частичное положительное решение.
В одном английском переводе Гильберт спрашивает:
«Когда мы занимаемся исследованием основ науки, мы должны установить систему аксиом, которая содержит точное и полное описание отношений, существующих между элементарными идеями этой науки. ... Но прежде всего я хочу обозначить следующий как наиболее важный среди многочисленных вопросов, которые могут быть заданы относительно аксиом: доказать, что они не противоречивы, то есть что определенное число логических шагов, основанных на них, никогда не может привести к противоречивым результатам. В геометрии доказательство совместимости аксиом может быть осуществлено путем построения подходящего поля чисел таким образом, чтобы аналогичные отношения между числами этого поля соответствовали геометрическим аксиомам. ... С другой стороны, необходим прямой метод для доказательства совместимости арифметических аксиом». [1]
Утверждение Гильберта иногда понимают неправильно, поскольку под «арифметическими аксиомами» он не имел в виду систему, эквивалентную арифметике Пеано, а более сильную систему с аксиомой полноты второго порядка. Система, для которой Гильберт просил доказательства полноты, больше похожа на арифметику второго порядка , чем на арифметику Пеано первого порядка.
В настоящее время общепринятой интерпретацией является то, что положительное решение второго вопроса Гильберта, в частности, предоставило бы доказательство того, что арифметика Пеано непротиворечива.
Существует множество известных доказательств того, что арифметика Пеано непротиворечива, которые могут быть выполнены в сильных системах, таких как теория множеств Цермело–Френкеля . Однако они не дают решения второго вопроса Гильберта, поскольку тот, кто сомневается в непротиворечивости арифметики Пеано, вряд ли примет аксиомы теории множеств (которые гораздо сильнее) для доказательства ее непротиворечивости. Таким образом, удовлетворительный ответ на проблему Гильберта должен быть выполнен с использованием принципов, которые были бы приемлемы для того, кто еще не верит, что PA непротиворечива. Такие принципы часто называют финитными, потому что они полностью конструктивны и не предполагают завершенной бесконечности натуральных чисел. Вторая теорема Гёделя о неполноте (см. теоремы Гёделя о неполноте ) накладывает строгие ограничения на то, насколько слабой может быть финитная система, при этом доказывая непротиворечивость арифметики Пеано.
Вторая теорема Гёделя о неполноте показывает, что невозможно провести какое-либо доказательство того, что арифметика Пеано непротиворечива, в рамках самой арифметики Пеано. Эта теорема показывает, что если единственными приемлемыми процедурами доказательства являются те, которые могут быть формализованы в рамках арифметики, то на призыв Гильберта к доказательству непротиворечивости нельзя ответить. Однако, как объясняют Нагель и Ньюман (1958), все еще есть место для доказательства, которое не может быть формализовано в арифметике: [2]
В 1936 году Генцен опубликовал доказательство того, что арифметика Пеано непротиворечива. Результат Генцена показывает, что доказательство непротиворечивости может быть получено в системе, которая намного слабее теории множеств.
Доказательство Генцена осуществляется путем назначения каждому доказательству в арифметике Пеано порядкового числа , основанного на структуре доказательства, причем каждый из этих порядков меньше ε 0 . [4] Затем он доказывает с помощью трансфинитной индукции по этим порядковым числам, что никакое доказательство не может прийти к противоречию. Метод, используемый в этом доказательстве, может также использоваться для доказательства результата устранения сечения для арифметики Пеано в более сильной логике, чем логика первого порядка, но само доказательство непротиворечивости может быть выполнено в обычной логике первого порядка с использованием аксиом примитивно-рекурсивной арифметики и принципа трансфинитной индукции. Тейт (2005) дает теоретико-игровую интерпретацию метода Генцена.
Доказательство непротиворечивости Генцена инициировало программу порядкового анализа в теории доказательств. В этой программе формальным теориям арифметики или теории множеств присваиваются порядковые числа , которые измеряют силу непротиворечивости теорий. Теория не сможет доказать непротиворечивость другой теории с более высоким порядковым номером доказательства теории.
Хотя теоремы Гёделя и Генцена теперь хорошо поняты сообществом математической логики, не сформировалось единого мнения о том, отвечают ли эти теоремы (или каким образом) на вторую проблему Гильберта. Симпсон (1988) утверждает, что теорема Гёделя о неполноте показывает, что невозможно получить финитные доказательства непротиворечивости сильных теорий. [5] Крайзель (1976) утверждает, что хотя результаты Гёделя подразумевают, что нельзя получить финитное синтаксическое доказательство непротиворечивости, семантические (в частности, второго порядка ) аргументы могут быть использованы для убедительных доказательств непротиворечивости. Детлефсен (1990) утверждает, что теорема Гёделя не препятствует доказательству непротиворечивости, поскольку ее гипотезы могут не применяться ко всем системам, в которых может быть выполнено доказательство непротиворечивости. [6] Доусон (2006) называет убеждение в том, что теорема Гёделя исключает возможность убедительного доказательства непротиворечивости, «ошибочным», ссылаясь на доказательство непротиворечивости, данное Генценом, и более позднее, данное Гёделем в 1958 году . [7]