к Оглавлению
Воспользуемся аксиомой для квантора существования (Д. Гильберт, П. Бернайс «Основания математики» Том 1, Глава 4 «Исчисление предикатов», Параграф 2 «Связанные переменные и правила для кванторов», Раздел 4 «Окончательная формулировка правил исчисления предикатов») и запишем аксиому для частного случая:
(P_0(«1=0», f(k)) = 1) ⇒ (∃y P_0(«1=0», y) = 1). Из 2х последних формул перейдем по правилу силлогизма к:
(P_0(«G», k) = 1) ⇒ (∃y P_0(«1=0», y) = 1), Используя правило вывода для квантора существования (см. вышеуказанный раздел в Д. Гильберт, П. Бернайс «Основания математики») получим:
(∃y P_0(«G», y) = 1) ⇒ (∃y P_0(«1=0», y) = 1), теперь перепишем это, используя принятое сокращение P(x) для (∃y P_0(x, y) = 1):
P(«G») ⇒ P(«1=0»)
Последняя формула и есть то, что нам оставалось доказать для завершения доказательства Второй теоремы Гёделя о неполноте.
Теорема доказана.
Теперь докажем, что недоказуема и P(«1=0»). То есть – что внутри непротиворечивой теории нет доказательства для отрицания утверждения о недоказуемости противоречия в данной непротиворечивой теории. Тогда ~P(«1=0») будет недоказуемо вместе со своим отрицанием и Вторая теорема Гёделя окажется вариантом Первой теоремы Гёделя о неполноте. Для доказательства нам потребуется «внешняя непротиворечивость», которую мы рассмотрели и сделали обзор о её доказательстве в предыдущем подразделе.
Если задуматься, то было бы странно, если бы в непротиворечивой теории было доказано утверждение о существовании в ней доказательства противоречия. Очевидно, что у нас есть недоказуемость противоречия для каждого конкретного доказательства k:
P_0(«1=0», k) = 0, откуда:
~( P_0(«1=0», k) = 1 )
В силу внешней непротиворечивости у нас «потенциально доказано» и
∀ x ~( P_0(«1=0», x) = 1 ), откуда «потенциально доказано»:
~∃ x ( P_0(«1=0», x) = 1 ), откуда «потенциально доказано»:
~P («1=0»)
Это всё означает, что теория Пеано (да и любая достаточно выразительная внешне непротиворечивая теория) может быть расширена аксиомой о непротиворечивости исходной (до расширения) теории. И никаких противоречий не возникнет.
А это значит, что и в исходной (до расширения) теории не было доказано P(«1=0»), что, собственно, мы и доказывали. Значит, во внешне непротиворечивой теории недоказуемо ни утверждение о её (теории) непротиворечивости, ни отрицание этого утверждения.
