Sztuczka Rossera - Rosser's trick

Twierdzenie o rzadkości liczb pierwszych znajduje się w twierdzeniu Rossera . Ogólne wprowadzenie do twierdzeń o niezupełności znajduje się w twierdzeniach o niezupełności Gödla .

W logice matematycznej , podstęp Rosser jest to sposób okazuje niezupełności twierdzenia Gödla bez założenia, że teoria rozważane jest ω spójne (Smorynski 1977, str 840;. Mendelson 1977, 160 str.). Metoda ta została wprowadzona przez J. Barkley Rossera w 1936 roku, jako ulepszenie oryginalnego dowodu Gödla na twierdzenia o niezupełności, opublikowanego w 1931 roku.

Podczas gdy oryginalny dowód Gödla używa zdania, które mówi (nieformalnie) „To zdanie nie jest dowodliwe”, sztuczka Rossera wykorzystuje formułę, która mówi: „Jeśli to zdanie jest dowodliwe, istnieje krótszy dowód jego negacji”.

tło

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

Dowód Gödla pokazuje, że dla każdej takiej teorii istnieje formuła, która ma zamierzone znaczenie, która jest kodem liczby naturalnej (liczba Gödla) dla formuły i jest liczbą Gödla dla dowodu, z aksjomatów , formuły zakodowanej przez . (W pozostałej części tego artykułu nie ma rozróżnienia między liczbą i formułą zakodowaną przez , a cyfrą kodującą formułę jest oznaczona ). Ponadto formuła jest zdefiniowana jako . Ma na celu zdefiniowanie zestawu formuł, które można udowodnić z . ${\ Displaystyle \ Operatorname {Dowód} _ {T} (x, y)}$${\displaystyle y}$${\displaystyle x}$${\displaystyle T}$${\displaystyle y}$${\displaystyle y}$${\displaystyle y}$${\displaystyle \phi}$${\displaystyle \#\phi}$${\ Displaystyle \ Operatorname {Pvbl} _ {T} (y)}$${\ Displaystyle \ istnieje x \ nazwa operatora {dowód} _ {T} (x, y)}$${\displaystyle T}$

Z założeń wynika również, że jest on w stanie zdefiniować funkcję negacji , z właściwością, że jeśli jest kodem formuły, to jest kodem formuły . Funkcja negacji może przyjmować dowolną wartość dla danych wejściowych, które nie są kodami formuł. ${\displaystyle T}$${\ Displaystyle {\ tekst {neg}} (y)}$${\displaystyle y}$${\displaystyle \phi}$${\ Displaystyle {\ tekst {neg}} (y)}$${\displaystyle \neg \phi}$

Zdanie Gödla tej teorii jest formułą , czasami oznaczaną , taką, która dowodzi  ↔ . Dowód gödla pokazuje, że jeśli jest niesprzeczny, to nie może udowodnić swojego zdania gödla; ale aby pokazać, że negacja zdania gödla jest również niedowodliwa, konieczne jest dodanie silniejszego założenia, że ​​teoria jest -spójna , a nie tylko niesprzeczna. Dowodzi na przykład teoria , w której PA to aksjomaty Peano . Rosser (1936) skonstruował inne zdanie samoodnoszące się, które może być użyte do zastąpienia zdania gödla w dowodzie Gödla, eliminując potrzebę założenia ω-spójności. ${\displaystyle T}$${\displaystyle \phi}$${\ Displaystyle G_ {T}}$${\displaystyle T}$${\displaystyle \phi}$${\ Displaystyle \ neg \ operatorname {Pvbl} _ {T} (\ # \ phi)}$${\displaystyle T}$${\ Displaystyle T = {\ tekst {PA}} + \ neg {\ tekst {G}} _ {PA}}$${\ Displaystyle \ neg G_ {T}}$

Zdanie Rossera

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

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

${\ Displaystyle \ Operatorname {Dowód} _ {T} ^ {R} (x, y) \ równoważny \ operatorname {Dowód} _ {T} (x, y) \ ziemia \ l nie \ istnieje z \ leq x [\ operatorname {Dowód} _{T}(z,\nazwa operatora {neg} (y))],}$

co oznacza że

${\ Displaystyle \ l nie \ operatorname {dowód} _ {T} ^ {R} (x, y) \ równoważny \ operatorname {dowód} _ {T} (x, y) \ do \ istnieje z \ leq x [\ operatorname {Dowód} _{T}(z,\nazwa operatora {neg} (y))].}$

Ten zmodyfikowany predykat dowodu jest używany do zdefiniowania zmodyfikowanego predykatu dowodliwości : ${\ Displaystyle \ Operatorname {Pvbl} _ {T} ^ {R} (y)}$

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

Nieformalnie jest to twierdzenie, które można udowodnić za pomocą jakiegoś zakodowanego dowodu, tak że nie ma mniejszego zakodowanego dowodu negacji . Przy założeniu, że jest to niesprzeczne, dla każdej formuły formuła będzie obowiązywać wtedy i tylko wtedy , gdy jest słuszna, ponieważ jeśli istnieje kod dowodu , to (zgodnie ze spójnością ) nie ma kodu dowodu . Jednak i mają inne właściwości z punktu widzenia dowodliwości w . ${\ Displaystyle \ Operatorname {Pvbl} _ {T} ^ {R} (y)}$${\displaystyle y}$${\displaystyle x}$${\displaystyle y}$${\displaystyle T}$${\displaystyle \phi}$${\ Displaystyle \ Operatorname {Pvbl} _ {T} ^ {R} (\ # \ phi)}$${\ Displaystyle \ Operatorname {Pvbl} _ {T} (\ # \ phi)}$${\displaystyle \phi}$${\displaystyle T}$${\displaystyle \neg \phi}$${\ Displaystyle \ Operatorname {Pvbl} _ {T} (\ # \ phi)}$${\ Displaystyle \ Operatorname {Pvbl} _ {T} ^ {R} (\ # \ phi)}$${\displaystyle T}$

Bezpośrednią konsekwencją definicji jest to, że jeżeli zawiera tyle arytmetyki, to może okazać się, że dla każdej formuły , zakłada . Jest tak, ponieważ w przeciwnym razie są dwie liczby , kodujący dowodów i , odpowiednio, spełniające oba a . (W rzeczywistości wystarczy udowodnić, że taka sytuacja nie może dotyczyć dowolnych dwóch liczb, a także zawrzeć jakąś logikę pierwszego rzędu) ${\displaystyle T}$${\displaystyle \phi}$${\ Displaystyle \ Operatorname {Pvbl} _ {T} ^ {R} (\ phi)}$${\ Displaystyle \ neg \ operatorname {Pvbl} _ {T} ^ {R} ({\ tekst {neg}} (\ phi))}$${\displaystyle n,m}$${\displaystyle \phi}$${\displaystyle \neg \phi}$${\displaystyle n<m}$${\displaystyle m<n}$${\displaystyle T}$

Używając lematu diagonalnego , niech będzie formułą taką, że dowodzi ρ ↔ ¬ Pvbl${\ Displaystyle \ rho}$${\displaystyle T}$^R
_T(nr ρ).  ↔ . Formuła jest zdaniem Rossera teorii . ${\ Displaystyle \ rho}$${\ Displaystyle \ neg \ operatorname {Pvbl} _ {T} (\ # \ rho)}$${\ Displaystyle \ rho}$${\displaystyle T}$

Twierdzenie Rossera

Niech będzie efektywna, spójna teoria zawierająca wystarczającą ilość arytmetyki, ze zdaniem Rossera . Potem następują twierdzenia (Mendelson 1977, s. 160): ${\displaystyle T}$${\ Displaystyle \ rho}$

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

Aby to udowodnić, najpierw pokazujemy, że dla formuły i liczby , jeśli zachodzi, to dowodzi . Widać to w podobny sposób, jak w dowodzie Gödla pierwszego twierdzenia o niezupełności: dowodzi , związek między dwiema konkretnymi liczbami naturalnymi; jeden potem podchodzi wszystkich liczb naturalnych mniejszych niż jeden po drugim, i dla każdego , okaże się , ponownie, relację między dwoma numerami betonowych. ${\displaystyle y}$${\displaystyle e}$${\ Displaystyle \ Operatorname {Dowód} _ {T} ^ {R} (e, y)}$${\displaystyle T}$${\ Displaystyle \ Operatorname {Dowód} _ {T} ^ {R} (e, y)}$${\displaystyle T}$${\ Displaystyle \ Operatorname {Dowód} _ {T} (e, y)}$${\displaystyle z}$${\displaystyle e}$${\displaystyle z}$${\displaystyle T}$${\ Displaystyle \ neg \ operatorname {Dowód} _ {T} (z {\ tekst {(neg}} (y))}$

Założenie, które zawiera wystarczającą ilość arytmetyki (w rzeczywistości wymagana jest podstawowa logika pierwszego rzędu) zapewnia, że również w tym przypadku dowodzi . ${\displaystyle T}$${\displaystyle T}$${\ Displaystyle \ Operatorname {Pvbl} _ {T} ^ {R} (y)}$

Co więcej, jeśli jest niesprzeczny i dowodzi , to istnieje kodowanie liczbowe dla dowodu w , a nie ma kodowania liczbowego dla dowodu negacji w . Dlatego trzyma, a tym samym dowodzi . ${\displaystyle T}$${\displaystyle \phi}$${\displaystyle e}$${\displaystyle T}$${\displaystyle \phi}$${\displaystyle T}$${\ Displaystyle \ Operatorname {Dowód} _ {T} ^ {R} (e, y)}$${\displaystyle T}$${\ Displaystyle \ Operatorname {Pvbl} _ {T} ^ {R} (\ # \ phi)}$

Dowód (1) jest podobny do dowodu Gödla pierwszego twierdzenia o niezupełności: Załóżmy , że dowodzi ; następnie wynika z poprzedniego opracowania, że dowodzi . Tak też udowadnia . Ale założyliśmy, że dowodzi , a to jest niemożliwe, jeśli jest spójne. Jesteśmy zmuszeni stwierdzić, że nie dowodzi . ${\displaystyle T}$${\ Displaystyle \ rho}$${\displaystyle T}$${\ Displaystyle \ Operatorname {Pvbl} _ {T} ^ {R} (\ # \ rho)}$${\displaystyle T}$${\ Displaystyle \ neg \ rho}$${\displaystyle T}$${\ Displaystyle \ rho}$${\displaystyle T}$${\displaystyle T}$${\ Displaystyle \ rho}$

Dowód (2) używa również szczególnej formy . Załóżmy , że dowodzi ; następnie wynika z poprzedniego opracowania, że dowodzi . Ale z bezpośredniej konsekwencji definicji predykatu dowodliwości Rossera, wspomnianej w poprzednim podrozdziale, wynika, że dowodzi . Tak też udowadnia . Ale założyliśmy, że dowodzi , a to jest niemożliwe, jeśli jest spójne. Jesteśmy zmuszeni stwierdzić, że nie dowodzi . ${\ Displaystyle \ Operatorname {Dowód} _ {T} ^ {R}}$${\displaystyle T}$${\ Displaystyle \ neg \ rho}$${\displaystyle T}$${\ Displaystyle \ operatorname {Pvbl} _ {T} ^ {R} ({\ tekst {neg}} \ # (\ rho))}$${\displaystyle T}$${\ Displaystyle \ neg \ operatorname {Pvbl} _ {T} ^ {R} (\ # \ rho)}$${\displaystyle T}$${\ Displaystyle \ rho}$${\displaystyle T}$${\ Displaystyle \ neg \ rho}$${\displaystyle T}$${\displaystyle T}$${\ Displaystyle \ neg \ rho}$

Bibliografia

• Mendelson (1977), Wprowadzenie do logiki matematycznej
• Smorynski (1977), „Twierdzenia o niezupełności”, w Handbook of Mathematical Logic , Jon Barwise , Ed., 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. JSTOR  2269028 .

Linki zewnętrzne

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