1я та 2я теореми Геделя про неповноту арифметики
Якщо теорія суперечлива, то в ній є твердження [math]F[/math], що доведено [math]F[/math] і [math]\neg F[/math].
Скористаємося формулою [math]\neg F \rightarrow F \rightarrow \beta[/math] .
якщо, якою б не була формула [math]P(x)[/math] з вільною змінною [math]x[/math] , така, що для будь-якого натурального числа [math]p[/math] доведено [math]P (p)[/math] ,
то формула [math] \ exists p \ neg P (p) [/ math] недоведена.
Розглянемо формулу, що виводиться [math]x=x \rightarrow x=x[/math] . При підстановці будь-якого натурального числа замість [math]x[/math] формула як і раніше виводиться: [math]\overline = \overline \rightarrow \overline=\overline[/math] . Значить, по [math] \ omega [/ math] -несуперечності формула [math] \ exists p \ neg (x = x \ rightarrow x = x) [/ math] невиводима.
Отже, теорія несуперечлива (оскільки у суперечливій теорії виводиться будь-яка формула).
Нехай формула [math]F[/math] із вільною змінною «x» має геделевий номер [math]f[/math] . Тоді визначимо рекурсивне ставлення [math]W_1[/math] , таке, що [math]W_1(f,p)[/math] істинно тоді і тільки тоді, коли [math]p[/math] є геделевий номер доказу [math] ]F(f)[/math] , тобто докази самозастосування [math]F[/math] . Тобто, у деякому наближенні це буде формула виду:
[math]W_1(f,p) := Free(f,[/math] «[math]x[/math] » [math]) \& Proof (Sub(f,[/math]) [[math]x[/math]»[math],Num(f)),p)[/math].
Розглянемо формулу [math] \ forall p \ neg W_1 (f, p) [/ math]. Нехай [math]w[/math] — її геделів номер. Тоді розглянемо формулу [math]\forall p\neg W_1(\overline,p)[/math]
1. Нехай формула [math]\forall p\neg W_1(\overline, p)[/math] доказується. Тоді знайдеться геделів номер її доказу[math]p[/math] , і значить [math]W_1(\overline,\overline
)[/math] . З іншого боку, за схемою аксіом для квантора загальності та правил Modus Ponens з припущення можна показати [math]\neg W_1(\overline,\overline
)[/math] . Отже, виходить, що формальна арифметика є суперечливою, що не відповідає припущенню.
2. Нехай [math]\vdash \neg \forall p \neg W_1 (\overline,p)[/math] . Отже, [math]\vdash \exists p W_1 (\overline,p)[/math] . Значить, по [math] \ omega [/ math] -несуперечності знайдеться таке натуральне число [math] p [/ math], що [math] \ vdash W_1 (\ overline, \ overline
)[/math] : інакше, якщо [math]\vdash \neg W_1 (\overline,\overline
)[/math] для будь-якого натурального [math]p[/math] , то по [math]\omega[/math] -несуперечності [math]\exists p \neg \neg W_1(\overline,p)[/math ] недоказово (нагадаємо, що [math]W_1[/math] виразно у формальній арифметиці, отже, для будь-якої пари [math]f[/math] і [math]p[/math] ми повинні мати або доказ [math]W_1 (\overline,\overline
)[/math] , або підтвердження заперечення цього).
Якщо знайдеться [math]p[/math] , що [math]W_1(w,p)[/math] , то [math]\vdash \forall p \neg W_1(w,p)[/math] . Отже, доведено і [math]\neg \exists p \neg \neg W_1 (w,p)[/math] . Отже, формальна арифметика суперечлива, що неможливо через припущення про неї
Формула [math] \ forall p \ neg W_1 (w, p) [/ math], кажучи простою мовою, стверджує власну недоказовість. Ми показали, що ця формула (за умови [math]\omega[/math] -несуперечності формальної арифметики) справді недоведена — отже, вірна. Таким чином, ми знайшли деякий вираз у формальній арифметиці, який є істинним, але недоказовим, і тим самим показали, що якщо формальна арифметика[math]\omega[/math] -несуперечлива, вона неповна.
У даному міркуванні використовується складне поняття [math]\omega[/math] -несуперечності, що бентежить. Теорема Геделя у вигляді Россера знімає цю складність.
Розглянемо ставлення [math] W_2 (f, p) [/ math] - [math] f [/ math] і [ math] p [/ math] складаються відносно [math] W_2 [/ math] тоді і тільки тоді, коли [math]p[/math] — геделевий номер доказузапереченнясамозастосування [math]f[/math] (якщо [math]F[/math] — формула з геделевим номером [math]f[/math] ] , то [math] p [/ math] - номер доказу [ math] \ neg F (f) [/ math] ). Ми можемо визначити його аналогічно [math] W_1 (w, p) [/ math].
Тоді розглянемо таку формулу [math]R(a)[/math] : [math]\forall x (W_1(a,x) \rightarrow \exists y(y \lt x \& W_2(a,y))) [/ Math] . Неформальною мовою вона стверджує, що для будь-якого доказу самозастосування певної формули з номером [math]a[/math] знайдеться доказ (та ще й з меншим номером геделя) заперечення цієї формули. Ну і за традицією застосуємо її до свого номера [math]r[/math]. Уважний розгляд цієї ситуації призводить до наступної теореми.
Аналог I теореми Геделя про неповноту [ред.]
Пояснимо, що це означає. Так як будь-яка мова програмування еквівалентна машині Тьюринга, то все пов'язане з ним кодується в логіці першого порядку з аксіомами Пеано (для цього достатньо, щоб програма вміла додавати до одиницю і викликати підпрограми), тому можна в термінах програм отримувати твердження, еквівалентні тим, що будував Ґедель.
Можна переформулювати теорему так: неможливо довести, що [math] p(x) = \perp [/math] .
Тоді напишемо таку програму:
знайдеться така формула [math]F[/math] , що як вона сама, і їїзаперечення
Позначимо геделевий номер [math]R[/math] за [math]r[/math]. Як формула [math]F[/math] візьмемо формулу [math]R(r)[/math] .
Розглянемо варіанти. Нехай [math]F[/math] доведено, тобто. [math] R (r) [/ math] істинно, тобто. [math]\forall x (W_1 (\overline,x) \rightarrow \exists y (y \lt x \& W_2 (\overline,y)))[/math] істинно. Отже, є такий [math]x[/math] , що [math]\exists y (y \lt x \& W_2 (\overline,y))[/math] істинно. Отже, знайдеться такий [math]y[/math] , що [math]W_2 (\overline,y)[/math] , тобто спростування [math]r[/math] з меншим номером. Тому формула [math]R(r)[/math] істинною, а значить і доведеною, бути не може.
Нехай докаузімо [math]\neg F[/math] . Нехай [math] p [/ math] - Геделевий номер доказу. Якщо так, то [math] W_2 (r, p) [/ math] істинно. По несуперечності формальної арифметики це означає, що [math]W_1(r,x)[/math] за будь-якого [math]x[/math] хибно (інакше виявиться, що знайдуться як доказ, так і спростування [math]R(r ) [/ Math]). Оскільки відношення [math]W_1 (r,x)[/math] виразне у формальній арифметиці, то доведено [math]\neg W_1 (\overline,\overline)[/math] за будь-якого [math]x[/math] ( тобто ніякий [math]x[/math] не є доказом [math]R(r)[/math] ). Як окремий випадок, [math]\neg W_1 (\overline,\overline)[/math] доведено для всіх [math]x[/math] , що не перевищують [math]p[/math] , тому доведено [math]\ neg W_1 (\overline,1) \& \neg W_1 (\overline,2) \& . \& \neg W_1 (\overline,\overline
)[/math] . Звідси можна показати доказ формули [math] x \le p \rightarrow \neg W_1 (\overline,x)[/math] . Позначимо цю формулу за [math]P_\le(x)[/math].
Розглянемо формулу [math](x \ge p) \rightarrow \exists y(y \le x \& W_2(\overline,y))[/math] Формула стверджує наступне: «якщо деякий [math]x[/math] більше ніж [math]p[/math] , то знайдеться такий [math]y[/math] , менший [math] x [/ math], що [math] W_2 (r, y) [/ math] ». Очевидно, що дана формула є істинною, адже якщо ми візьмемо [math]p[/math] як таке [math]y[/math] , то [math]W_2 (r,p)[/math] істинно за припущенням. Позначимо розглянуту формулу за [math]P_\ge(x)[/math] і зауважимо, що вона доведена.
Легко показати, що з цих тверджень і з того, що [math]x \le p \vee x \ge p[/math] можна вивести [math]\neg W_1 (\overline,x) \vee \exists y ( y \lt x \& W_2 (\overline,y))[/math] , а звідси - [math]\forall x (W_1 (\overline,x) \rightarrow \exists y (y \lt x \& W_2 (\overline, y))) [/ math], тобто [math] F [/ math]. Проте, ми припустили доказовість [math]\neg F[/math] , і з нього, вивели [math]F[/math] , тобто. показали суперечливість формальної арифметики. Значить,
[math]\neg F[/math] також недоведено, якщо арифметика несуперечлива.