Warunki dowodliwości Hilberta-Bernaya

W logice matematycznej warunki dowodzenia Hilberta-Bernaysa , nazwane na cześć Davida Hilberta i Paula Bernaysa , to zestaw wymagań dla sformalizowanych predykatów dowodliwości w formalnych teoriach arytmetyki (Smith 2007: 224).

Warunki te są używane w wielu dowodach drugiego twierdzenia o niezupełności Kurta Gödla . Są one również ściśle związane z aksjomatami logiki możliwości udowodnienia .

Warunki

Niech $T$ będzie formalną teorią arytmetyki ze sformalizowanym predykatem dowodliwości $Prov(n)$ , który jest wyrażony jako wzór $T$ z jedną zmienną liczbową swobodną. Dla każdego wzoru $φ$ w teorii niech $#(φ)$ będzie liczbą Gödla $φ$ . Warunki dowodliwości Hilberta-Bernaysa to:

Jeśli $T$ dowodzi zdania $φ,$ to $T$ dowodzi $Prov(#(φ))$ .
Dla każdego zdania $φ$ , $T$ dowodzi $Przyw(#(φ)) \to Przyw(#(Przyw(#(φ))))$
$T$ dowodzi, że $Prow(#(φ \to ψ))$ i $Prow(#(φ))$ implikują $Prow(#(ψ))$

Zauważ, że $Prov$ jest predykatem liczb i jest predykatem dowodliwości w tym sensie, że zamierzona interpretacja $Prov(#(φ))$ jest taka, że istnieje liczba, która koduje dowód $φ$ . Formalnie to, co jest wymagane od $Prov,$ to powyższe trzy warunki.

W bardziej zwięzłej notacji logiki możliwości udowodnienia , pozwalając $\ Displaystyle T}$ oznaczenie „ $dowodzi$ φ $\ Displaystyle \ varphi}$ " i $varphi}$ oznaczają ${\ Displaystyle {\ tekst {Prz.}} (\ # (\ varphi))}$ :

${\ Displaystyle (T \ vdash \ varphi) \ do (T \ vdash \ Box \ varphi)}$
${\ Displaystyle T \ vdash (\ Box \ phi \ do \ Box \ Box \ phi)}$
${\ Displaystyle T \ vdash \ Box (\ varphi \ do \ psi) \ do \ Box \ varphi \ do \ Box \ psi}$

Użyj do udowodnienia twierdzeń Gödla o niezupełności

Warunki sprawdzalności Hilberta-Bernaysa w połączeniu z lematem o przekątnej pozwalają w krótkim czasie udowodnić oba twierdzenia Gödla o niezupełności. Rzeczywiście, główny wysiłek w dowodach Godla polegał na wykazaniu, że te warunki (lub równoważne) i diagonalny lemat są spełnione dla arytmetyki Peano; po ich ustaleniu dowód można łatwo sformalizować.

$przekątnej$ , istnieje wzór taki, że ${\ Displaystyle T \ Vdash \ rho \ leftrightarrow \ neg Prov (\ #$ .

Dowód pierwszego twierdzenia Gödla o niezupełności

Dla pierwszego twierdzenia potrzebne są tylko pierwszy i trzeci warunek.

Warunek, że $T$ jest ω-spójny , jest uogólniony przez warunek, że jeśli dla każdego wzoru $φ$ , jeśli $T$ dowodzi $Prov(#(φ))$ , to $T$ dowodzi $φ$ . Zauważ, że to rzeczywiście odnosi się do $ω$ -spójnego $T$ , ponieważ $Prov(#(φ))$ oznacza, że istnieje liczba kodująca dowód $φ$ , a jeśli $T$ jest $ω$ -spójny, to przechodząc przez wszystkie liczby naturalne, można faktycznie znaleźć takie konkretny numer $a$ , a następnie można użyć $a$ do skonstruowania rzeczywistego dowodu $φ$ w $T$ .

Załóżmy, że T mógłby udowodnić ${\ displaystyle \ rho}$ . Mielibyśmy wtedy następujące twierdzenia w $T$ :

${\ Displaystyle T \ Vdash \ rho}$
${\ Displaystyle T \ Vdash \ neg Prov (\ # (\ rho))}$ (przez konstrukcję i twierdzenie 1 ) ${\ Displaystyle \ rho }$
${\ Displaystyle T \ Vdash Prov (\ # (\ rho))}$ (zgodnie z warunkiem nr 1 i twierdzeniem 1)

Tak więc $T$ dowodzi zarówno ${\ Displaystyle Prov (\ # (\ rho))}$ i ${\ Displaystyle \ neg Prov (\ # (\ rho ))}$ . Ale jeśli $T jest$ $dowodzi$ , jest to niemożliwe i jesteśmy zmuszeni stwierdzić, że $T$ nie .

Załóżmy teraz, że $T$ mógł udowodnić ${\ displaystyle \ neg \ rho}$ . Mielibyśmy wtedy następujące twierdzenia w $T$ :

${\ Displaystyle T \ Vdash \ neg \ rho}$
${\ Displaystyle T \ Vdash Prov (\ # (\ rho))}$ (przez konstrukcję ${\ Displaystyle \ rho}$ i twierdzenie 1)
${\ Displaystyle T \ Vdash \ rho}$ (przez spójność ω)

Zatem $T$ dowodzi zarówno ${\ displaystyle \ rho},$ jak i ${\ displaystyle \ neg \ rho}$ . $że$ jeśli $T$ jest spójne, jest to niemożliwe i jesteśmy zmuszeni stwierdzić, $T$ nie .

Podsumowując, $T$ nie może udowodnić ani ${\ displaystyle \ rho}$ , ani ${\ displaystyle \ neg \ rho}$ .

Używając sztuczki Rossera

Korzystając ze sztuczki Rossera , nie trzeba zakładać, że $T$ jest $ω$ -spójne. Należałoby jednak wykazać, że pierwszy i trzeci warunek dowodliwości jest spełniony dla $Prov R$ , predykatu Rossera o dowodliwości, a nie dla naiwnego predykatu o dowodliwości Prz. Wynika to z faktu, że dla każdej formuły $φ$ , $Prov(#(φ))$ zachodzi wtedy i tylko wtedy, gdy zachodzi $Prov R.$

Dodatkowym zastosowanym warunkiem jest to, że $T$ dowodzi, że $Prov R (#(φ))$ implikuje $\negProv R (#(\negφ))$ . Warunek ten obowiązuje dla każdego $T$ , które obejmuje logikę i bardzo podstawową arytmetykę (jak omówiono w sztuczce Rossera #Zdanie Rossera ).

Korzystając ze sztuczki Rossera, $ρ$ jest definiowane przy użyciu predykatu możliwości udowodnienia Rossera zamiast naiwnego predykatu możliwości udowodnienia. Pierwsza część dowodu pozostaje niezmieniona, z wyjątkiem tego, że predykat możliwości udowodnienia jest tam również zastąpiony predykatem Rossera.

Druga część dowodu nie wykorzystuje już spójności ω i została zmieniona na następującą:

Załóżmy, że $T$ mógłby udowodnić ${\ displaystyle \ neg \ rho}$ . Mielibyśmy wtedy następujące twierdzenia w $T$ :

${\ Displaystyle T \ Vdash \ neg \ rho}$
${\ Displaystyle T \ Vdash Prov ^ {R} (\ # (\ rho))}$ (przez konstrukcję i twierdzenie 1 ) ${\ Displaystyle \ rho }$
${\ Displaystyle T \ Vdash \ neg Prov ^ {R} (\ # (\ neg \ rho))}$ (z twierdzenia 2 i dodatkowego warunku następującego po definicji predykatu dowodliwości Rossera)
${\ Displaystyle T \ Vdash Prov ^ {R} (\ # (\ neg \ rho))}$ (według warunku nr 1 i twierdzenia 1)

Zatem $T$ dowodzi zarówno ${\ Displaystyle Prov ^ {R} (\ # (\ neg \ rho)}}$ i $\neg Prov ^{R}(\#(\neg \rho ))$ . Ale jeśli $T$ jest niesprzeczne, jest to niemożliwe i jesteśmy zmuszeni dojść do wniosku, że $T$ nie dowodzi ${\ Displaystyle \ neg \ rho}$ .

Drugie twierdzenie

Zakładamy, że $T$ dowodzi własnej zgodności, tj. że:

{\ Displaystyle T \ Vdash \ neg Prov (\ # (1 = 0))}

.

Dla każdego wzoru $φ$ :

{\ Displaystyle T \ Vdash \ neg \ varphi \ rightarrow (\ varphi \ rightarrow (1 = 0))}

(przez eliminację negacji )

Można pokazać za pomocą warunku nr. 1 na tym ostatnim twierdzeniu, po którym następuje wielokrotne użycie warunku nr. 3, że:

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

A używając $T$ dowodzącego własnej spójności wynika, że:

{\ Displaystyle T \ Vdash Prov (\ # (\ neg \ varphi)} \ rightarrow \ neg Prov (\ # (\ varphi ))}

Teraz użyjemy tego, aby pokazać, że $T$ nie jest spójne:

${\ Displaystyle T \ Vdash Prov (\ #(\neg Prov(\#(\rho )))\rightarrow \neg Prov(\#(Prov(\#(\rho )))} ($ po $T$ ${\ Displaystyle \ varphi = Prov (\ # (\ rho)}$ } )
${\ Displaystyle T \ Vdash \ rho \ rightarrow \ neg Prov (\ # (\ rho))}$ (przez konstrukcję ${\ Displaystyle \ rho}$ )
${\ Displaystyle T \ Vdash Prov (\ # (\ rho \ rightarrow \ neg Prov (\ # (\ rho)}) }$ (z warunku nr 1 i twierdzenia 2)
${\ Displaystyle T \ Vdash Prov (\ # (\ rho)) \ rightarrow Prov (\#(\neg Prov(\#(\rho )))}$ (z warunku nr 3 i twierdzenia 3)
${\ Displaystyle T \ Vdash Prov (\ # (\ rho)) \ strzałka w prawo \ neg Prov(\#(Prov(\#(\rho )))}$ (z twierdzeń 1 i 4)
${\ Displaystyle T \ Vdash Prov (\ # (\ rho)) \ rightarrow Prov ( \#(Prov(\#(\rho )))}$ (zgodnie z warunkiem nr 2)
${\ Displaystyle T \ Vdash \ neg Prov (\ # (\ rho))}$ (według twierdzeń 5 i 6)
${\ Displaystyle T \ Vdash \ neg Prov (\ # (\ rho)) \ strzałka w prawo \ rho}$ (przez konstrukcję ${\ Displaystyle \ rho}$ )
${\ Displaystyle T \ Vdash \ rho}$ (według twierdzeń 7 i 8)
${\ Displaystyle T \ Vdash Prov (\ # (\ rho))}$ (z warunku 1 i twierdzenia 9)