Условия доказуемости Гильберта – Бернейса

В математической логике , условия доказуемости Гильберта-Бернейса названные в честь Дэвида Гильберта и Пола Бернейса , представляют собой набор требований к формализованным предикатам доказуемости в формальных теориях арифметики (Smith 2007:224).

Эти условия используются во многих доказательствах Курта Гёделя о второй теоремы неполноте . Они также тесно связаны с аксиомами логики доказуемости .

Условия

Пусть $T$ — формальная теория арифметики с формализованным предикатом доказуемости $Prov(n)$ , который выражается как формула $T$ с одной свободной числовой переменной. Для каждой формулы $φ$ в теории пусть $#(φ)$ — число Гёделя для $φ$ . Условия доказуемости Гильберта – Бернейса:

Если $T$ доказывает предложение $φ$ , то $T$ доказывает $Prov(#(φ))$ .
Для каждого предложения $T$ φ $доказывает$ Prov $(#(φ)) \to Prov(#(Prov(#(φ))))$
$T$ доказывает, что $Prov(#(φ \to ψ))$ и $Prov(#(φ))$ влекут $Prov(#(ψ))$

Обратите внимание, что $Prov$ — это предикат чисел, и это предикат доказуемости в том смысле, что предполагаемая интерпретация $Prov(#(φ))$ состоит в том, что существует число, которое кодирует доказательство $φ$ . требуются $Формально от Prov$ три вышеуказанных условия.

В более кратком обозначении логики доказуемости , позволяя $T\vdash \varphi$ обозначать " $T$ доказывает $\varphi$ " и $\Box \varphi$ обозначать ${\text{Prov}}(\#(\varphi ))$ :

$(T\vdash \varphi )\to (T\vdash \Box \varphi )$
$T\vdash (\Box \phi \to \Box \Box \phi )$
$T\vdash (\Box (\varphi \to \psi )\to \Box \varphi \to \Box \psi )$

Использование при доказательстве теорем Гёделя о неполноте.

Условия доказуемости Гильберта – Бернейса в сочетании с диагональной леммой позволяют вкратце доказать обе теоремы Гёделя о неполноте. Действительно, основная задача доказательств Гёделя заключалась в том, чтобы показать, что эти условия (или эквивалентные) и диагональная лемма справедливы для арифметики Пеано; как только они установлены, доказательство можно легко формализовать.

Используя диагональную лемму, существует формула $\rho$ такой, что $T\Vdash \rho \leftrightarrow \neg Prov(\#(\rho ))$ .

Доказательство первой теоремы Гёделя о неполноте.

Для первой теоремы нужны только первое и третье условия.

Условие того, что $T$ ω - непротиворечиво, обобщается условием, что если для каждой формулы $φ$ , если $T$ доказывает $Prov(#(φ))$ , то $T$ доказывает $φ$ . Обратите внимание, что это действительно справедливо для $ω$ -согласованного $T,$ поскольку $Prov(#(φ))$ означает, что существует числовое кодирование для доказательства $φ$ , и если $T$ - согласован $ω$ , то, пройдя через все натуральные числа, можно фактически найти такое конкретное число $a$ , и тогда можно использовать $a,$ построить фактическое доказательство $φ$ в $T.$ чтобы

Предположим, Т мог бы доказать $\rho$ . Тогда мы имели бы следующие теоремы в $T$ :

$T\Vdash \rho$
$T\Vdash \neg Prov(\#(\rho ))$ (по построению $\rho$ и теорема 1)
$T\Vdash Prov(\#(\rho ))$ (по условию № 1 и теореме 1)

Таким образом, $T$ доказывает оба $Prov(\#(\rho ))$ и $\neg Prov(\#(\rho ))$ . Но если $Т$ непротиворечиво, это невозможно, и мы вынуждены заключить, что $Т$ не доказывает $\rho$ .

Теперь предположим, что $Т$ мог бы доказать $\neg \rho$ . Тогда мы имели бы следующие теоремы в $T$ :

$T\Vdash \neg \rho$
$T\Vdash Prov(\#(\rho ))$ (по построению $\rho$ и теорема 1)
$T\Vdash \rho$ (по ω-согласованности)

Таким образом, $T$ доказывает оба $\rho$ и $\neg \rho$ . Но если $Т$ непротиворечиво, это невозможно, и мы вынуждены заключить, что $Т$ не доказывает $\neg \rho$ .

В заключение, $T$ не может доказать ни $\rho$ ни $\neg \rho$ .

Использование трюка Россера

Используя прием Россера , не нужно предполагать, что $T$ - $ω$ непротиворечиво. Однако нужно будет показать, что первое и третье условия доказуемости выполняются для $Prov. Р$ , предикат доказуемости Россера, а не для наивного предиката доказуемости Prov. Это следует из того, что для любой формулы $справедливо$ φ $Prov(#(φ))$ тогда и только тогда, когда $Prov Р$ держит.

Дополнительное условие состоит в том, что $T$ доказывает, что $Prov. Р (#(φ))$ подразумевает $\negProv Р (#(\negφ))$ . Это условие справедливо для любого $T$ , которое включает в себя логику и очень простую арифметику (как это описано в трюке Россера #Предложение Россера ).

Используя прием Россера, $ρ$ определяется с использованием предиката доказуемости Россера вместо предиката наивной доказуемости. Первая часть доказательства остается неизменной, за исключением того, что предикат доказуемости и там заменяется предикатом Россера.

Вторая часть доказательства больше не использует ω-непротиворечивость и изменена на следующую:

Предположим, $Т$ мог бы доказать $\neg \rho$ . Тогда мы имели бы следующие теоремы в $T$ :

$T\Vdash \neg \rho$
$T\Vdash Prov^{R}(\#(\rho ))$ (по построению $\rho$ и теорема 1)
$T\Vdash \neg Prov^{R}(\#(\neg \rho ))$ (по теореме 2 и дополнительному условию, следующему за определением предиката доказуемости Россера)
$T\Vdash Prov^{R}(\#(\neg \rho ))$ (по условию № 1 и теореме 1)

Таким образом, $T$ доказывает оба $Prov^{R}(\#(\neg \rho ))$ и $\neg Prov^{R}(\#(\neg \rho ))$ . Но если $Т$ непротиворечиво, это невозможно, и мы вынуждены заключить, что $Т$ не доказывает $\neg \rho$ .

Вторая теорема

Мы предполагаем, что $T$ доказывает свою непротиворечивость, т.е. что:

T\Vdash \neg Prov(\#(1=0))

.

Для каждой формулы $φ$ :

T\Vdash \neg \varphi \rightarrow (\varphi \rightarrow (1=0))

(путем исключения отрицания )

Это можно показать, используя условие №. 1 по последней теореме с последующим повторным использованием условия №. 3, что:

T\Vdash Prov(\#(\neg \varphi ))\rightarrow (Prov(\#(\varphi ))\rightarrow Prov(\#(1=0)))

И используя $T,$ доказывающую его собственную непротиворечивость, следует, что:

T\Vdash Prov(\#(\neg \varphi ))\rightarrow \neg Prov(\#(\varphi ))

Теперь мы используем это, чтобы показать, что $T$ несовместим:

$T\Vdash Prov(\#(\neg Prov(\#(\rho )))\rightarrow \neg Prov(\#(Prov(\#(\rho )))$ (после того, как $T$ доказывает свою непротиворечивость, с $\varphi =Prov(\#(\rho ))$ )
$T\Vdash \rho \rightarrow \neg Prov(\#(\rho ))$ (по построению $\rho$ )
$T\Vdash Prov(\#(\rho \rightarrow \neg Prov(\#(\rho )))$ (по условию № 1 и теореме 2)
$T\Vdash Prov(\#(\rho ))\rightarrow Prov(\#(\neg Prov(\#(\rho )))$ (по условию № 3 и теореме 3)
$T\Vdash Prov(\#(\rho ))\rightarrow \neg Prov(\#(Prov(\#(\rho )))$ (по теоремам 1 и 4)
$T\Vdash Prov(\#(\rho ))\rightarrow Prov(\#(Prov(\#(\rho )))$ (по условию №2)
$T\Vdash \neg Prov(\#(\rho ))$ (по теоремам 5 и 6)
$T\Vdash \neg Prov(\#(\rho ))\rightarrow \rho$ (по построению $\rho$ )
$T\Vdash \rho$ (по теоремам 7 и 8)
$T\Vdash Prov(\#(\rho ))$ (по условию 1 и теореме 9)