Sztuczka Rossera

Aby zapoznać się z twierdzeniem o rzadkości liczb pierwszych, zobacz twierdzenie Rossera .

W logice matematycznej sztuczka Rossera jest metodą dowodzenia twierdzeń Gödla o niezupełności bez założenia, że ​​rozpatrywana teoria jest ω-spójna ( Smoryński 1977, s. 840; Mendelson 1977, s. 160). Metoda ta została wprowadzona przez J. Barkleya Rossera w 1936 roku jako ulepszenie oryginalnego dowodu twierdzeń o niezupełności Gödla, który został opublikowany w 1931 roku.

Podczas gdy oryginalny dowód Gödla używa zdania, które mówi (nieformalnie) „Tego zdania nie da się udowodnić”, sztuczka Rossera wykorzystuje formułę, która mówi: „Jeśli to zdanie jest do udowodnienia, istnieje krótszy dowód jego zaprzeczenia”.

Tło

Sztuczka Rossera zaczyna się od założeń twierdzenia Gödla o niezupełności. Wybiera się teorię $, która jest$ , spójna i zawiera wystarczający fragment elementarnej arytmetyki.

Dowód Gödla pokazuje, że dla każdej takiej teorii istnieje formuła $} _ {T} (x, y$ Dowód $}$ jest naturalnym kodem liczbowym (liczbą Gödla) dla formuły i $displaystyle$ liczbą Gödla jako dowodem na podstawie aksjomatów formuły zakodowanej przez $y}$${\ displaystyle y}$ . (W dalszej części tego artykułu nie ma rozróżnienia między liczbą $,$ formułą zakodowaną przez a liczba kodująca formułę $displaystyle$ oznaczona $\ Displaystyle \ # \ phi$$\ phi}$$T$ jest jako ${\ Displaystyle \ istnieje x \ operatorname {Dowód} _ {T} (x, y)}$ . Ma na celu zdefiniowanie zestawu formuł możliwych do udowodnienia na podstawie ${\ displaystyle T}$ .

Założenia na ${\ displaystyle T}$ pokazują również, że jest w stanie zdefiniować funkcję negacji ${\ Displaystyle {\ tekst {neg}} (y)}$ z właściwością, że ${\ displaystyle y}$ jest kodem dla formuły, $\$ następnie $Displaystyle {\ tekst {neg}} (y)}$ jest kodem dla formuły ${\ Displaystyle \ neg \ phi}$ . Funkcja negacji może przyjąć dowolną wartość dla danych wejściowych, które nie są kodami formuł.

$T$$displaystyle T}$ teorii jest formułą $fi}$ czasami oznaczaną $,$ taką, że $\$ udowadnia . ${\ displaystyle$ ↔ ${\ Displaystyle \ neg \ operatorname {Pvbl} _ {T} (\ # \ phi)}$ . Dowód Gödla pokazuje, że jeśli ${\ displaystyle T}$ jest spójny, to nie może udowodnić swojego zdania Gödla; ale aby pokazać, że negacja zdania Gödla również nie jest dowodliwa, konieczne jest dodanie silniejszego założenia, że ​​teoria jest ω-konsystencja , a nie tylko spójność. Na $,$ teoria której aksjomaty ${\ Displaystyle \ neg G_ {T}}$ . Rosser (1936) skonstruował inne zdanie odnoszące się do samego siebie, którego można użyć do zastąpienia zdania Gödla w dowodzie Gödla, eliminując potrzebę zakładania spójności ω.

Zdanie Rossera

Dla ustalonej teorii arytmetycznej , niech ${\ Displaystyle \ operatorname {Dowód} _ {T} (x, y)}$$($ zanegować ${neg}}(x)}$$\ Displaystyle {\$ będzie powiązanym predykatem dowodowym i funkcją negacji.

Zmodyfikowany predykat dowodu Dowód ${\ Displaystyle \ operatorname {Dowód} _ {T} ^ {R} (x, y)}$ zdefiniowany jako:

$${\ Displaystyle \ nazwa operatora {Dowód} _ {T} ^ {R} (x, y) \ równoważnik \ nazwa operatora {Dowód} _ {T} (x, y) \ ziemia \ lnot \ istnieje z \ równoważnik x [\ nazwa operatora {Dowód} _{T}(z,\nazwa_operatora {neg} (y))],}$$

co oznacza że

$${\ Displaystyle \ lnot \ nazwa operatora {Dowód} _ {T} ^ {R} (x, y) \ równoważnik \ nazwa operatora {Dowód} _ {T} (x, y) \ do \ istnieje z \ równoważnik x [\ nazwa operatora {Dowód} _{T}(z,\nazwa_operatora {neg} (y))].}$$

Ten zmodyfikowany predykat dowodowy jest używany do zdefiniowania zmodyfikowanego predykatu potwierdzalności ${\ Displaystyle \ operatorname {Pvbl} _ {T} ^ {R} (y)$ }

$${\ Displaystyle \ nazwa operatora {Pvbl} _ {T} ^ {R} (y) \ równoważnik \ istnieje x \ nazwa operatora {Dowód} _ {T} ^ {R} (x, y).}$$

Nieformalnie $_ {T} ^ {R} (y)}$$x }$ jest twierdzeniem, że można udowodnić za pomocą jakiegoś zakodowanego dowodu $displaystyle$ tak, że nie ma mniejszego zakodowanego dowodu negacji ${\ displaystyle y}$ . $jest$ założeniu, że $formuły$ , dla każdej formuła ${\ Displaystyle \ nazwa operatora {Pvbl} _ {T} ^ {R} (\ # \ phi)}$ będzie obowiązywać wtedy i tylko wtedy, gdy $\ # \ phi)}$${\ Displaystyle \ nazwa operatora {Pvbl} _ {T}$$)$ zachodzi, ponieważ jeśli istnieje kod dla dowodu $.$ to (zgodnie z konsekwencją nie ma kodu dla dowodu z ${\ Displaystyle \ neg \ phi}$ . Jednak ${\ Displaystyle \ nazwa operatora {Pvbl} _ {T} (\ # \ phi)}$ i ${\ Displaystyle \ nazwa operatora {Pvbl} _ {T} ^ {R} ( \#\ phi )}$ mają różne właściwości z punktu widzenia możliwości udowodnienia w ${\ displaystyle T}$ .

Bezpośrednią konsekwencją definicji jest to, że jeśli $zawiera$$)$$\ Displaystyle \ operatorname {Pvbl} _ {T} ^ {R} (\ phi)}$ może udowodnić, że dla każdej formuły Pvbl implikuje ${\ Displaystyle \ neg \ operatorname {Pvbl} _ {T} ^ {R} ({\ tekst {neg} }(\fi))}$ . ${\ displaystyle n <m}$$liczby$$razie$ istnieją dwie $oba$ i , spełniające i ${\ displaystyle m <n}$ . (W rzeczywistości ${\ displaystyle T}$ musi tylko udowodnić, że taka sytuacja nie może zachodzić dla dowolnych dwóch liczb, a także uwzględnić logikę pierwszego rzędu)

Korzystając z lematu o przekątnej $udowadnia$$niech$ będzie ^RT
_formułą taką, że ↔ ¬ Pvbl (# ρ). ${\ Displaystyle \ rho}$ ↔ ${\ Displaystyle \ neg \ operatorname {Pvbl} _ {T} (\ # \ rho)}$ . Formuła jest zdaniem Rossera $displaystyle$ . $T}$ .

Twierdzenie Rossera

Niech $będzie$$Rossera$ ilość arytmetyki, ze zdaniem . Następnie następujący chwyt (Mendelson 1977, s. 160):

1. ${\ displaystyle T}$ nie dowodzi ${\ displaystyle \ rho}$
2. ${\ displaystyle T}$ nie dowodzi ${\ Displaystyle \ neg \ rho}$

Aby to udowodnić, najpierw pokazuje się, że dla wzoru $Dowód} _ {T } ^ {R} (e, y)}$${$ ⁡ ( $operatorname$ utrzymuje się, a następnie $udowadnia$$e, y )}$ { T} ^ {R} . Jest to pokazane w podobny sposób, jak w dowodzie Gödla pierwszego twierdzenia o niezupełności: ${\ displaystyle T}$ dowodzi ${\ Displaystyle \ operatorname {Dowód} _ {T} (e, y)}$ , relacja między dwiema konkretnymi liczbami naturalnymi; następnie przechodzi się po kolei przez wszystkie liczby naturalne mniejsze niż $z$ {\ displaystyle e} i dla każdego $T.$$z$ } ${\ Displaystyle T}$ dowodzi ${\ Displaystyle \ neg \ operatorname {Dowód} _ {T} (z, {\ tekst {(neg}} (y))$ } znowu relacja między dwiema konkretnymi liczbami.

Założenie, że $Pvbl} } _{T}^{R}(y)}$ R ⁡ ${$$\$ w takim przypadku.

Ponadto, jeśli jest $,$ i udowadnia to istnieje liczba $\ displaystyle$ jego dowód w $T}$ i nie ma kodowania liczbowego T { $\$ dla dowodu zaprzeczenia ${\ displaystyle \ phi}$ w ${\ displaystyle T}$ . Dlatego ${\ Displaystyle \ operatorname {Pvbl} _ {T}^{R}(\#\phi)}$$^ {R} (e, y)}$ się, a zatem udowadnia $R$ .

Dowód (1) jest podobny do tego w dowodzie Gödla pierwszego twierdzenia o niezupełności: Załóżmy, że $\$ ρ $displaystyle \ rho}$ ; następnie z poprzedniego opracowania wynika, że ​​Pvbl $\ Displaystyle \ operatorname {Pvbl} _ {T} ^ {R} (\ # \ rho$${$ ) Zatem dowodzi to również, $}$${\ Displaystyle \ neg \ rho$ . Ale założyliśmy, $że to dowodzi$ i $jest$ niemożliwe, $spójne$ . Jesteśmy zmuszeni stwierdzić, że $\ rho}$ nie dowodzi $displaystyle$ .

Dowód (2) wykorzystuje również szczególną formę ${\ displaystyle \ operatorname {Dowód} _ {T} ^ {R}}$ . Załóżmy, że ${\ displaystyle T}$ udowadnia ${\ Displaystyle \ neg \ rho}$ ; następnie z poprzedniego opracowania wynika, że ​​Pvbl $_ {T} ^ {R} ({\ text {$$}$ . Ale z bezpośredniej konsekwencji definicji predykatu dowodliwości Rossera, wspomnianej w poprzedniej sekcji, wynika, że $​​udowadnia$$operatorname {Pvbl} _ { T}^{R}(\#\rho )}$ ( . Zatem dowodzi to również $\ displaystyle \ rho$$}$ . Ale założyliśmy, że $displaystyle$ T $T }$ i jest to niemożliwe, jeśli $jest$ . Jesteśmy zmuszeni stwierdzić, że to $\ displaystyle$ dowodzi $T$ }

• Mendelson (1977), Wprowadzenie do logiki matematycznej
•   Smoryński (1977), „Twierdzenia o niezupełności”, w: Handbook of Mathematical Logic , Jon Barwise , wyd., North Holland, 1982, ISBN 0-444-86388-5
•    Barkley Rosser (wrzesień 1936). „Rozszerzenia niektórych twierdzeń Gödla i Churcha” . Dziennik logiki symbolicznej . 1 (3): 87–91. doi : 10.2307/2269028 . JSTOR 2269028 . S2CID 36635388 .

Linki zewnętrzne

• Avigad (2007), „ Obliczalność i niezupełność ”, notatki z wykładów.