1я и 2я теоремы Геделя о неполноте арифметики — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 4: Строка 4:
  
 
[[Категория: Математическая логика]]
 
[[Категория: Математическая логика]]
 +
 +
= 1я и 2я теоремы Геделя о неполноте арифметики =
 +
 +
{{Определение
 +
|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>
 +
 +
{{Теорема
 +
|about = Первая теорема Геделя о неполноте арифметики
 +
|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>.
 +
Внимательное рассмотрение этой ситуации приводит к следующей теореме.
 +
 +
{{Теорема
 +
|about=Теорема Геделя в форме Россера
 +
|statement=
 +
Если формальная арифметика непротиворечива, то
 +
найдется такая формула <tex>F</tex>, что как она сама, так и ее отрицание
 +
недоказуемы.
 +
|proof=
 +
Обозначим геделев номер <tex>R</tex> за <tex>r</tex>. В качестве формулы <tex>F</tex> возьмем формулу <tex>R(r)</tex>.
 +
 +
Рассмотрим варианты. Пусть <tex>F</tex> доказуемо, т.е. <tex>R(r)</tex> истинно,
 +
т.е. <tex>\forall x (W_1 (\overline{r},x) \rightarrow \exists y (y < x \& W_2 (\overline{r},y)))</tex>
 +
истинно. Значит, есть такой <tex>x</tex>, что <tex>\exists y (y < x \& W_2 (\overline{r},y))</tex> истинно.
 +
Значит, найдется такой <tex>y</tex>, что <tex>W_2 (\overline{r},y)</tex>, т.е., что существует опровержение
 +
<tex>r</tex> с меньшим номером. Поэтому формула <tex>R(r)</tex> истинной, а значит и доказуемой,
 +
быть не может.
 +
 +
Пусть докауземо <tex>\neg F</tex>. Пусть <tex>p</tex> — геделев номер доказательства.
 +
Раз так, то <tex>W_2 (r,p)</tex> истинно. По непротиворечивости формальной арифметики
 +
это значит, что <tex>W_1 (r,x)</tex> при любом <tex>x</tex> ложно (иначе окажется, что
 +
найдутся как доказательство, так и опровержение <tex>R(r)</tex>). Поскольку
 +
отношение <tex>W_1 (r,x)</tex> выразимо в формальной арифметике, то
 +
доказуемо <tex>\neg W_1 (\overline{r},\overline{x})</tex> при любом <tex>x</tex> (т.е. никакой из <tex>x</tex> не является
 +
доказательством <tex>R(r)</tex>). Как частный случай, <tex>\neg W_1 (\overline{r},\overline{x})</tex> доказуемо для
 +
всех <tex>x</tex>, не превышающих <tex>p</tex>, поэтому доказуемо
 +
<tex>\neg W_1 (\overline{r},1) \& \neg W_1 (\overline{r},2) \& ... \& \neg W_1 (\overline{r},\overline{p})</tex>.
 +
Отсюда можно показать доказуемость формулы <tex>x \le p \rightarrow \neg W_1 (\overline{r},x)</tex>.
 +
Обозначим эту формулу за <tex>P_\le(x)</tex>.
 +
 +
Рассмотрим формулу <tex>(x \ge p) \rightarrow \exists y (y \le x \& W_2 (\overline{r},y))</tex>
 +
Формула утверждает следующее: «если некоторый <tex>x</tex> больше чем <tex>p</tex>, то найдется
 +
такой <tex>y</tex>, меньший <tex>x</tex>, что <tex>W_2 (r,y)</tex>». Очевидно, что данная формула истинна,
 +
ведь если мы возьмем <tex>p</tex> в качестве такого <tex>y</tex>, то <tex>W_2 (r,p)</tex> истинно
 +
по предположению.  Обозначим рассмотренную формулу за <tex>P_\ge(x)</tex> и заметим,
 +
что она также доказуема.
 +
 +
Легко показать, что из этих утверждений и из того, что <tex>x \le p \vee x \ge p</tex>,
 +
можно вывести <tex>\neg W_1 (\overline{r},x) \vee \exists y (y < x \& W_2 (\overline{r},y))</tex>,
 +
а отсюда — <tex>\forall x (W_1 (\overline{r},x) \rightarrow \exists y (y < x \& W_2 (\overline{r},y)))</tex>,
 +
то есть <tex>F</tex>. Однако, мы предположили доказуемость <tex>\neg F</tex>, и исходя из него,
 +
вывели <tex>F</tex>, т.е. показали противоречивость формальной арифметики. Значит,
 +
<tex>\neg F</tex> также недоказуемо, если арифметика непротиворечива.
 +
}}
 +
 +
{{Теорема
 +
|about=Вторая теорема Геделя о неполноте арифметики
 +
|statement=
 +
Если в формальной арифметике удастся доказать ее непротиворечивость, то
 +
на основании этого доказательства можно построить противоречие в формальной
 +
арифметике.
 +
|proof=
 +
Рассмотрим только схему доказательства. Возьмем <tex>Consis</tex>, некоторое
 +
утверждение, которое показывает непротиворечивость арифметики, т.е.
 +
показывает отсутствие такой формулы <tex>S</tex>, что и <tex>S</tex> и <tex>\neg S</tex> доказуемы
 +
(его можно выписать:
 +
<tex>\forall s ((\forall p \neg Proof (s,p)) \vee (\forall p \neg Proof (</tex>«<tex>\neg \$s</tex>»<tex>, p)))</tex>)
 +
 +
Тогда рассмотрим формулу <tex>Consis \rightarrow (\forall p \neg W_1(\overline{w},p))</tex>.
 +
Данная формула в точности соответствует условию 1й теоремы Геделя
 +
о неполноте арифметики (если формальная арифметика непротиворечива,
 +
то <tex>\forall p \neg W_1(\overline{w},p)</tex> недоказуемо; напомним, что <tex>w</tex> ведь и есть
 +
геделев номер формулы <tex>\forall p \neg W_1(x,p)</tex> со свободной переменной <tex>x</tex>).
 +
Рассуждение, доказывающее 1ю теорему, можно формализовать, получив доказательство
 +
данной импликации. Теперь, если у нас будет доказательство утверждения <tex>Consis</tex>,
 +
то по правилу Modus Ponens мы также получаем доказательство утверждения <tex>(\forall p \neg W_1(\overline{w},p))</tex>.
 +
Однако, существование такого доказательства влечет за собой противоречивость формальной арифметики.
 +
}}
 +
 +
Последним в данном разделе заметим, что данные доказательства естественно
 +
обобщаются на случай произвольной формальной теории, включающей формальную
 +
арифметику. Достаточно только расширить правила, проверяющие доказательства
 +
формул на корректность (т.е. добавить в них новые аксиомы, схемы аксиом,
 +
и правила или схемы правил вывода).

Версия 22:18, 14 января 2012

<< >>

1я и 2я теоремы Геделя о неполноте арифметики

Определение:
Мы будем называть теорию непротиворечивой, если не найдется такой формулы [math]F[/math], что доказуемо как [math]F[/math], так и [math]\neg F[/math].


Лемма:
Если теория противоречива, то в ней доказуемо любая формула.
Доказательство:
[math]\triangleright[/math]

Если теория противоречива, то в ней есть утверждение [math]F[/math], что доказуемо [math]F[/math] и [math]\neg F[/math].

Воспользуемся доказуемой формулой [math]\neg F \rightarrow F \rightarrow \beta[/math].
[math]\triangleleft[/math]


Определение:
Мы будем называть теорию [math]\omega[/math]-непротиворечивой,

если, какова бы ни была формула [math]P(x)[/math] со свободной переменной [math]x[/math], такая, что для любого натурального числа [math]p[/math] доказуемо [math]P(p)[/math],

то формула [math]\exists p \neg P(p)[/math] недоказуема.


Лемма:
[math]\omega[/math]-непротиворечивость влечет непротиворечивость.
Доказательство:
[math]\triangleright[/math]

Рассмотрим выводимую формулу [math]x=x \rightarrow x=x[/math]. При подстановке любого натурального числа вместо [math]x[/math] формула будет по-прежнему выводима: [math]\overline{k} = \overline{k} \rightarrow \overline{k}=\overline{k}[/math]. Значит, по [math]\omega[/math]-непротиворечивости формула [math]\exists p \neg (x=x \rightarrow x=x)[/math] невыводима.

Значит, теория непротиворечива (поскольку в противоречивой теории выводится любая формула).
[math]\triangleleft[/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{w},p)[/math]

Теорема (Первая теорема Геделя о неполноте арифметики):
1. Если формальная арифметика непротиворечива, то недоказуемо [math]\forall p \neg W_1(\overline{w},p)[/math].
2. Если формальная арифметика [math]\omega[/math]-непротиворечива, то недоказуемо [math]\neg \forall p \neg W_1(\overline{w},p)[/math].
Доказательство:
[math]\triangleright[/math]

1. Пусть формула [math]\forall p \neg W_1(\overline{w},p)[/math] доказуема. Тогда найдется геделев номер ее доказательства [math]p[/math], и значит [math]W_1(\overline{w},\overline{p})[/math]. С другой стороны, по схеме аксиом для квантора всеобщности и правилу Modus Ponens из предположения можно показать [math]\neg W_1(\overline{w},\overline{p})[/math]. Значит, получается, что формальная арифметика противоречива, что не соответствует предположению.

2. Пусть [math]\vdash \neg \forall p \neg W_1 (\overline{w},p)[/math]. Значит, [math]\vdash \exists p W_1 (\overline{w},p)[/math]. Значит, по [math]\omega[/math]-непротиворечивости найдется такое натуральное число [math]p[/math], что [math]\vdash W_1(\overline{w},\overline{p})[/math]: иначе, если [math]\vdash \neg W_1 (\overline{w},\overline{p})[/math] для любого натурального [math]p[/math], то по [math]\omega[/math]-непротиворечивости [math]\exists p \neg \neg W_1(\overline{w},p)[/math] недоказуемо (напомним, что [math]W_1[/math] выразимо в формальной арифметике, значит, для любой пары [math]f[/math] и [math]p[/math] мы должны иметь либо доказательство [math]W_1(\overline{f},\overline{p})[/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]\omega[/math]-непротиворечивости.
[math]\triangleleft[/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]. Внимательное рассмотрение этой ситуации приводит к следующей теореме.

Теорема (Теорема Геделя в форме Россера):
Если формальная арифметика непротиворечива, то

найдется такая формула [math]F[/math], что как она сама, так и ее отрицание

недоказуемы.
Доказательство:
[math]\triangleright[/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{r},x) \rightarrow \exists y (y \lt x \& W_2 (\overline{r},y)))[/math] истинно. Значит, есть такой [math]x[/math], что [math]\exists y (y \lt x \& W_2 (\overline{r},y))[/math] истинно. Значит, найдется такой [math]y[/math], что [math]W_2 (\overline{r},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{r},\overline{x})[/math] при любом [math]x[/math] (т.е. никакой из [math]x[/math] не является доказательством [math]R(r)[/math]). Как частный случай, [math]\neg W_1 (\overline{r},\overline{x})[/math] доказуемо для всех [math]x[/math], не превышающих [math]p[/math], поэтому доказуемо [math]\neg W_1 (\overline{r},1) \& \neg W_1 (\overline{r},2) \& ... \& \neg W_1 (\overline{r},\overline{p})[/math]. Отсюда можно показать доказуемость формулы [math]x \le p \rightarrow \neg W_1 (\overline{r},x)[/math]. Обозначим эту формулу за [math]P_\le(x)[/math].

Рассмотрим формулу [math](x \ge p) \rightarrow \exists y (y \le x \& W_2 (\overline{r},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{r},x) \vee \exists y (y \lt x \& W_2 (\overline{r},y))[/math], а отсюда — [math]\forall x (W_1 (\overline{r},x) \rightarrow \exists y (y \lt x \& W_2 (\overline{r},y)))[/math], то есть [math]F[/math]. Однако, мы предположили доказуемость [math]\neg F[/math], и исходя из него, вывели [math]F[/math], т.е. показали противоречивость формальной арифметики. Значит,

[math]\neg F[/math] также недоказуемо, если арифметика непротиворечива.
[math]\triangleleft[/math]
Теорема (Вторая теорема Геделя о неполноте арифметики):
Если в формальной арифметике удастся доказать ее непротиворечивость, то

на основании этого доказательства можно построить противоречие в формальной

арифметике.
Доказательство:
[math]\triangleright[/math]

Рассмотрим только схему доказательства. Возьмем [math]Consis[/math], некоторое утверждение, которое показывает непротиворечивость арифметики, т.е. показывает отсутствие такой формулы [math]S[/math], что и [math]S[/math] и [math]\neg S[/math] доказуемы (его можно выписать: [math]\forall s ((\forall p \neg Proof (s,p)) \vee (\forall p \neg Proof ([/math]«[math]\neg \$s[/math]»[math], p)))[/math])

Тогда рассмотрим формулу [math]Consis \rightarrow (\forall p \neg W_1(\overline{w},p))[/math]. Данная формула в точности соответствует условию 1й теоремы Геделя о неполноте арифметики (если формальная арифметика непротиворечива, то [math]\forall p \neg W_1(\overline{w},p)[/math] недоказуемо; напомним, что [math]w[/math] ведь и есть геделев номер формулы [math]\forall p \neg W_1(x,p)[/math] со свободной переменной [math]x[/math]). Рассуждение, доказывающее 1ю теорему, можно формализовать, получив доказательство данной импликации. Теперь, если у нас будет доказательство утверждения [math]Consis[/math], то по правилу Modus Ponens мы также получаем доказательство утверждения [math](\forall p \neg W_1(\overline{w},p))[/math].

Однако, существование такого доказательства влечет за собой противоречивость формальной арифметики.
[math]\triangleleft[/math]

Последним в данном разделе заметим, что данные доказательства естественно обобщаются на случай произвольной формальной теории, включающей формальную арифметику. Достаточно только расширить правила, проверяющие доказательства формул на корректность (т.е. добавить в них новые аксиомы, схемы аксиом, и правила или схемы правил вывода).