Введение
Согласованность аксиом арифметики
В математике вторая проблема Гильберта была сформулирована Давидом Гильбертом в 1900 году как одна из его 23 проблем. Она требует доказательства непротиворечивости арифметики – отсутствия внутренних противоречий. Гильберт указал, что аксиомами, которые он рассматривал для арифметики, были аксиомы, представленные в [название работы], которые включают аксиому полноты второго порядка. В 1930-х годах Курт Гёдель и Герхард Гентцен получили результаты, проливающие новый свет на эту проблему. Некоторые полагают, что теоремы Гёделя дают отрицательный ответ на вопрос о разрешимости проблемы, в то время как другие рассматривают доказательство Гентцена как частичное положительное решение.
In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that arithmetic is consistent – free of any internal contradictions. Hilbert stated that the axioms he considered for arithmetic were the ones given in , which include a second order completeness axiom. In the 1930s, Kurt Gödel and Gerhard Gentzen proved results that cast new light on the problem. Some feel that Gödel's theorems give a negative solution to the problem, while others consider Gentzen's proof as a partial positive solution.
Теорема о неполноте Гёделя
Вторая теорема о неполноте Гёделя показывает, что невозможно доказать непротиворечивость арифметики Пеано средствами самой арифметики Пеано. Эта теорема демонстрирует, что если единственными допустимыми методами доказательства являются те, которые могут быть формализованы в арифметике, то призыв Гильберта к доказательству непротиворечивости остаётся без ответа. Однако, как будет показано, всё ещё остаётся место для доказательства, которое нельзя формализовать в арифметике: "Этот впечатляющий результат анализа Гёделя не следует понимать превратно: он не исключает метаматематического доказательства непротиворечивости арифметики. Он исключает лишь доказательство непротиворечивости, которое можно было бы воспроизвести формальными выводами арифметики. Метаматематические доказательства непротиворечивости арифметики, по сути, были построены, в частности, Герхардом Гентценом, последователем школы Гильберта, в 1936 году, и впоследствии другими исследователями. Но эти метаматематические доказательства не могут быть представлены средствами арифметического исчисления; и поскольку они не являются финитистскими, они не достигают заявленных целей первоначальной программы Гильберта. Возможность построения финитистского абсолютного доказательства непротиворечивости арифметики не исключается результатами Гёделя. Гёдель показал, что не существует такого доказательства, которое можно было бы представить средствами арифметики. Его аргумент не исключает возможности строго финитистских доказательств, которые нельзя представить средствами арифметики. Однако, на сегодняшний день, похоже, никто не имеет чёткого представления о том, каким могло бы быть финитистское доказательство, которое нельзя было бы сформулировать в рамках арифметики."
"This imposing result of Godel's analysis should not be misunderstood: it does not exclude a meta mathematical proof of the consistency of arithmetic. What it excludes is a proof of consistency that can be mirrored by the formal deductions of arithmetic. Meta mathematical proofs of the consistency of arithmetic have, in fact, been constructed, notably by Gerhard Gentzen, a member of the Hilbert school, in 1936, and by others since then. But these meta mathematical proofs cannot be represented within the arithmetical calculus; and, since they are not finitistic, they do not achieve the proclaimed objectives of Hilbert's original program. The possibility of constructing a finitistic absolute proof of consistency for arithmetic is not excluded by Gödel’s results. Gödel showed that no such proof is possible that can be represented within arithmetic. His argument does not eliminate the possibility of strictly finitistic proofs that cannot be represented within arithmetic. But no one today appears to have a clear idea of what a finitistic proof would be like that is not capable of formulation within arithmetic."
Доказательство консистенции Гентцена
В 1936 году Гентцен опубликовал доказательство того, что арифметика Пеано является непротиворечивой. Результат Гентцена показывает, что доказательство непротиворечивости может быть получено в системе, значительно более слабой, чем теория множеств. Доказательство Гентцена строится путем присвоения каждому доказательству в арифметике Пеано порядкового числа, основанного на структуре этого доказательства, причем каждое из этих порядковых чисел меньше ε0. Затем он доказывает трансфинитной индукцией по этим порядковым числам, что ни одно доказательство не может завершиться противоречием. Метод, используемый в этом доказательстве, также может быть применен для доказательства теоремы об устранении отсечений для арифметики Пеано в логике, более сильной, чем логика первого порядка, однако само доказательство непротиворечивости может быть выполнено в обычной логике первого порядка, используя аксиомы примитивно рекурсивной арифметики и принцип трансфинитной индукции. Существует игровая интерпретация метода Гентцена. Доказательство непротиворечивости, предложенное Гентценом, положило начало программе порядкового анализа в теории доказательств. В рамках этой программы формальным теориям арифметики или теории множеств присваиваются порядковые числа, которые измеряют силу непротиворечивости этих теорий. Теория не сможет доказать непротиворечивость другой теории с более высоким доказательно-теоретическим порядковым числом.
Современные взгляды на состояние проблемы
Хотя теоремы Гёделя и Гентцена хорошо известны в сообществе математической логики, единого мнения о том, отвечают ли (и каким образом) эти теоремы на вторую проблему Гильберта, до сих пор не сложилось. утверждает, что теорема о неполноте Гёделя показывает невозможность построения финитарных доказательств непротиворечивости сильных теорий. утверждает, что, хотя результаты Гёделя подразумевают отсутствие финитарного синтаксического доказательства непротиворечивости, семантические (в частности, второго порядка) аргументы могут быть использованы для получения убедительных доказательств непротиворечивости. утверждает, что теорема Гёделя не исключает доказательство непротиворечивости, поскольку её предположения могут не относиться ко всем системам, в которых такое доказательство может быть выполнено. называет убеждение в том, что теорема Гёделя исключает возможность убедительного доказательства непротиворечивости, "неверным", ссылаясь на доказательство непротиворечивости, предложенное Гентценом, и более позднее доказательство, данное Гёделем в 1958 году.