313
правок
Изменения
Нет описания правки
[[Лекция 8 Геделева нумерация. Арифметизация доказательств | <<]][[Лекция 10 Теория множеств | >>]]
[[Категория: Математическая логика]]==Определения=={{Определение |definition=Мы будем называть теорию непротиворечивой, еслине найдется такой формулы <tex>F</tex>, что доказуемо как <tex>F</tex>, так и <tex>\neg F</tex>.}} {{Лемма|statement=Если теория противоречива, то в ней доказуемо любая формула.|proof=Если теория противоречива, то в ней есть утверждение <tex>F</tex>, что доказуемо <tex>F</tex> и <tex>\neg F</tex>.Воспользуемся доказуемой формулой <tex>\neg F \rightarrow F \rightarrow \beta</tex>.}} {{Определение|definition=Мы будем называть теорию <tex>\omega</tex>-непротиворечивой,если, какова бы ни была формула <tex>P(x)</tex> со свободной переменной <tex>x</tex>, такая, что для любого натурального числа <tex>p</tex> доказуемо <tex>P(p)</tex>, то формула <tex>\exists p \neg P(p)</tex> недоказуема.}} {{Лемма|statement=<tex>\omega</tex>-непротиворечивость влечет непротиворечивость.|proof=Рассмотрим выводимую формулу <tex>x=x \rightarrow x=x</tex>.При подстановке любого натурального числа вместо <tex>x</tex>формула будет по-прежнему выводима: <tex>\overline{k} = \overline{k} \rightarrow \overline{k}=\overline{k}</tex>.Значит, по <tex>\omega</tex>-непротиворечивости формула <tex>\exists p \neg (x=x \rightarrow x=x)</tex> невыводима.Значит, теория непротиворечива (поскольку в противоречивой теории выводится любая формула).}} Пусть формула <tex>F</tex> со свободной переменной «x» имеет геделев номер <tex>f</tex>. Тогда определим рекурсивное отношение <tex>W_1</tex>, такое, что <tex>W_1(f,p)</tex> истинно тогда и только тогда, когда <tex>p</tex> есть геделев номер доказательства <tex>F(f)</tex>, то есть доказательства самоприменения <tex>F</tex>. То есть в некоторомприближении это будет формула вида: <tex>W_1(f,p) := Free(f,</tex>«<tex>x</tex>»<tex>) \& Proof (Sub(f,</tex>«<tex>x</tex>»<tex>,Num(f)),p)</tex>. Рассмотрим формулу <tex>\forall p \neg W_1(f,p)</tex>. Пусть <tex>w</tex> — ее геделев номер. Тогда рассмотрим формулу <tex>\forall p \neg W_1(\overline{w},p)</tex> ==Первая теорема Геделя о неполноте арифметики=={{Теорема|statement=1. Если формальная арифметика непротиворечива, то недоказуемо <tex>\forall p \neg W_1(\overline{w},p)</tex>.<br>2. Если формальная арифметика <tex>\omega</tex>-непротиворечива, то недоказуемо <tex>\neg \forall p \neg W_1(\overline{w},p)</tex>.|proof=1. Пусть формула <tex>\forall p \neg W_1(\overline{w},p)</tex> доказуема. Тогда найдется геделев номер ее доказательства <tex>p</tex>, и значит <tex>W_1(\overline{w},\overline{p})</tex>. С другой стороны, по схеме аксиом для квантора всеобщности и правилу Modus Ponens из предположения можно показать <tex>\neg W_1(\overline{w},\overline{p})</tex>. Значит, получается, что формальная арифметика противоречива, что не соответствует предположению. 2. Пусть <tex>\vdash \neg \forall p \neg W_1 (\overline{w},p)</tex>. Значит, <tex>\vdash \exists p W_1 (\overline{w},p)</tex>. Значит, по <tex>\omega</tex>-непротиворечивости найдется такое натуральное число <tex>p</tex>, что<tex>\vdash W_1(\overline{w},\overline{p})</tex>: иначе, если <tex>\vdash \neg W_1 (\overline{w},\overline{p})</tex> для любого натурального <tex>p</tex>, то по <tex>\omega</tex>-непротиворечивости <tex>\exists p \neg \neg W_1(\overline{w},p)</tex> недоказуемо(напомним, что <tex>W_1</tex> выразимо в формальной арифметике, значит, для любой пары <tex>f</tex> и <tex>p</tex> мы должны иметь либо доказательство <tex>W_1(\overline{f},\overline{p})</tex>, либо доказательство отрицания этого). Раз найдется <tex>p</tex>, что <tex>W_1(w,p)</tex>, то <tex>\vdash \forall p \neg W_1 (w,p)</tex>.А, значит, доказуемо и <tex>\neg \exists p \neg \neg W_1 (w,p)</tex>. Значит, формальнаяарифметика противоречива, что невозможно в силу предположения о ее <tex>\omega</tex>-непротиворечивости.}} Формула <tex>\forall p \neg W_1(w,p)</tex>, говоря простым языком, утверждает собственную недоказуемость. Мы показали, что эта формула (при условии <tex>\omega</tex>-непротиворечивости формальной арифметики) действительно недоказуема — а, значит, верна. Таким образом, мы нашли некотороевыражение в формальной арифметике, которое истинно, но недоказуемо,и тем самым показали, что если формальная арифметика <tex>\omega</tex>-непротиворечива, то она неполна. В данном рассуждении используется сложное понятие<tex>\omega</tex>-непротиворечивости, что смущает. Теорема Геделя в форме Россера снимает эту сложность. Рассмотрим отношение <tex>W_2 (f,p)</tex> — <tex>f</tex> и <tex>p</tex> состоят в отношении <tex>W_2</tex> тогда и только тогда, когда<tex>p</tex> — геделев номер доказательства ''отрицания'' самоприменения <tex>f</tex> (если <tex>F</tex> — формула сгеделевым номером <tex>f</tex>, то <tex>p</tex> — номер доказательства <tex>\neg F(f)</tex>). Мы можем определить его аналогично <tex>W_1 (w,p)</tex>. Тогда рассмотрим такую формулу <tex>R(a)</tex>: <tex>\forall x (W_1 (a,x) \rightarrow \exists y (y < x \& W_2 (a,y)))</tex>.Неформальным языком она утверждает, что для любого доказательства самоприменения некоторой формулы с номером <tex>a</tex> найдется доказательство (да еще и с меньшим геделевым номером) отрицания этой формулы. Ну и по традиции применим ее к своему номеру <tex>r</tex>. Внимательное рассмотрение этой ситуации приводит к следующей теореме.===Аналог I теоремы Гёделя о неполноте==={{Теорема|statement = В разработкелюбой '''достаточно богатой системе''' существует истинное недоказуемое утверждение.|proof =Поясним, что это значит. Так как любой язык программирования эквивалентен [[Машина Тьюринга | машине Тьюринга]], то всё связанное с ним кодируется в [[Теории первого порядка | логике первого порядка]] с [[Классы_чисел#Аксиомы_Пеано | аксиомами Пеано]](для этого достаточно, чтобы программа умела прибавлять к числу единицу и вызывать подпрограммы), поэтому можно в терминах программ получать утверждения, эквивалентные тем, что строил Гёдель. Можно переформулировать теорему следующим образом: невозможно доказать, что <tex> p(x) = \perp </tex>.
