yandex rtb 1
ГоловнаЗворотній зв'язок
yande share

Математическая логика

6.7. Вторая теорема Геделя.

Определим Neg(x) так, что если х есть геделев номер формулы А, то Neg(x) есть геделев номер формулы ¬А. Функции Neg, очевидно, рекурсивна и, следовательно, представима в S некоторой формулой Neg(x1,x2). Введем предикат Pf(у,х), истиной тогда и только тогда, когда х есть геделев номер некоторой формулы А теории S, а у есть геделев номер некоторого вывода А в S. Предикат Pf примитивно рекурсивен, и по тому выразим в S с помощью некоторой формулы Pf(x1,x2)

Обозначим через Cons формулу 

x1x2x3x4¬(Pf(x1,x3)&Pf(x2,x4)&Neg(x3,x4)). Следовательно, т.е. в соответствии со стандартной интерпретацией, Cons выражает невозможность вывода в S какой-либо формулы вместе с её отрицанием и является истинной в том и только том случае, когда теория S непротиворечива. Иными словами, формулу Cons можно интерпретировать как утверждение непротиворечивости теории S. Вспомним теперь, что, в соответствии со стандартной интерпретацией, геделева неразрешимая формула G содержательно выражает свою собственную не выводимость. Тогда формула ConsG содержательно утверждает, что если теория S непротиворечива, то формула G  в ней не выводима. Но в этом и состоит первая часть теоремы Геделя. Математические рассуждения, доказывающие теорему Геделя, могут быть выражены и проведены средствами теории S,  так что в  результате оказывается возможным получить вывод формулы ConsG в теории S.(Доказательство этого утверждения см.у Гильберта и Бернайса [1939]). Итак, |-sConsG. Согласно теореме Геделя, однако, если теория S не противоречива, то формула G в ней не выводима. Отсюда следует, что если теория S непротиворечива, то в ней не выводима формула Cons; иными словами, если теория непротиворечива, то в ней не выводима некоторая формула, содержательно утверждающая непротиворечивость теории S. Этот результат носит название второй теоремы Геделя. Грубо говоря, эта теорема утверждает, что если теория S непротиворечива, то доказательство непротиворечивости теории не может быть проведено средствами самой теории S, т.е. всякое такое доказательство обязательно должно использовать не выразимые в S идеи или методы. Примерами могут служить доказательства непротиворечивости теории S, предложенные Генценом (1936,1938) и Шютте (1951), в некоторых применяются понятия и методы (например, один фрагмент теории счетных порядковых чисел), очевидно, не формализуемые средствами теории S.

 

43