Część 3: Twierdzenie G¨ odla
Antoni Kościelski 23 stycznia 2015
Spis treści
1 Arytmetyka Q i twierdzenie G¨odla 1
1.1 Definicje reprezentowalności . . . 1
1.1.1 Reprezentowalność funkcji . . . 1
1.1.2 Mocna reprezentowalność zbiorów . . . 2
1.1.3 Reprezentowalność zbiorów . . . 2
1.2 Reprezentowalność funkcji pierwotnie rekurencyjnych . . . 2
1.3 Kodowanie formuł i dowodów . . . 3
1.4 Oryginalny dowód twierdzenie G¨odla . . . 4
1.4.1 ω-niesprzeczność i reprezentowalność . . . . 4
1.4.2 Sformułowanie twierdzenia . . . 5
1.4.3 Lemat przekątniowy . . . 5
1.4.4 Ważny zbiór U . . . 5
1.4.5 Ciąg dalszy dowodu . . . 6
1.5 Dodatkowy wniosek . . . 7
2 Twierdzenie G¨odla według Churcha 7 2.1 Teza Churcha . . . 7
2.2 Twierdzenie o nierozstrzygalności arytmetyki . . . 9
2.3 Entscheidungsproblem . . . 9
2.4 Twierdzenie o niezupełności arytmetyki . . . 10
1 Arytmetyka Q i twierdzenie G¨ odla
Przypomnijmy, że jeżeli n jest liczbą naturalną, to n jest przedstawieniem liczby n w języku arytmetyki, rozumianym jako term zdefiniowany w następujący sposób:
0 = 0, 1 = 1 oraz n + 1 = n + 1.
1.1 Definicje reprezentowalności
1.1.1 Reprezentowalność funkcji
Niech T będzie teorią zapisaną w języku arytmetyki. O formule ϕ mówimy, że reprezentuje w teorii T funkcję f : Nk → N , jeżeli warunek f (n1, . . . , nk) = m implikuje, że
T ` ϕ[x1 ← n1] . . . [xk← nk] ⇔ y = m
1
dla wszystkich n1, . . . , nk, m ∈ N . Równoważnie tę definicję można wyrazić żąda- jąc, aby warunek f (n1, . . . , nk) = m implikował, że
T ` ϕ[x1 ← n1] . . . [xk ← nk][y ← m]
oraz
T ` ∃¬1y ϕ[x1 ← n1] . . . [xk← nk],
gdzie ∃¬1φ oznacza „istnieje najwyżej jeden element o własności φ”, czyli „każde dwa elementy o własności φ są równe”. Funkcja jest reprezentowalna w teorii T , jeżeli jest formuła reprezentująca tę funkcję w teorii T .
1.1.2 Mocna reprezentowalność zbiorów Formuła ϕ mocno reprezentuje zbiór X ⊆ Nk, jeżeli
1) warunek (n1, . . . , nk) ∈ X implikuje, że T ` ϕ[x1 ← n1] . . . [xk ← nk], 2) warunek (n1, . . . , nk) 6∈ X implikuje, że T ` ¬ϕ[x1 ← n1] . . . [xk← nk].
W oczywisty sposób definiujemy jeszcze zbiory mocno reprezentowalne. Mamy też
Lemat 1.1 Przypuśćmy, że T ` 0 6= 1. Zbiór X jest mocno reprezentowalny w T wtedy i tylko wtedy, gdy funkcja charakterystyczna chX jest reprezentowalna w T .
1.1.3 Reprezentowalność zbiorów
Formuła ϕ reprezentuje zbiór X ⊆ Nk, jeżeli równoważne są warunki (n1, . . . , nk) ∈ X oraz T ` ϕ[x1 ← n1] . . . [xk ← nk].
Jak zwykle definiujemy jeszcze zbiory reprezentowalne w teorii T . Dla takich zbiorów dowodzimy następujące własności:
Lemat 1.2 Jeżeli pewnien zbiór X 6= Nk jest reprezentowalny w teorii T , to T jest niesprzeczna. 2
Lemat 1.3 Jeżeli teoria T jest niesprzeczna, to każdy zbiór mocno reprezentowal- ny w T jest reprezentowalny w T . 2
1.2 Reprezentowalność funkcji pierwotnie rekurencyjnych
Symbolem Q oznaczamy prostą arytmetyką, złożoną z dziewięciu aksjomatów, zde- finiowaną w części 1, strona ??.
Lemat 1.4 Każda formuła
x < n + 1 ⇔ x = 0 ∨ x = 1 ∨ . . . ∨ x = n ma dowód w arytmetyce Q, a więc
Q ` x < n + 1 ⇔ x = 0 ∨ x = 1 ∨ . . . ∨ x = n.
Lemat 1.5 W arytmetyce Q i każdej obszerniejszej teorii są mocno reprezento- walne relacje równości, mniejszości i większości, a także ich dopełnienia (negacje).
Twierdzenie 1.6 W arytmetyce Q i każdej obszerniejszej teorii są reprezentowal- ne wszystkie funkcje pierwotnie rekurencyjne.
Wniosek 1.7 W arytmetyce Q i każdej obszerniejszej teorii są mocno reprezen- towalne wszystkie zbiory pierwotnie rekurencyjne.
1.3 Kodowanie formuł i dowodów
Oprócz ciągów, za pomocą liczb naturalnych będziemy kodować także znaki alfa- betu, za pomocą którego zapisujemy formuły języka arytmetyki, w tym symbole zmiennych indywiduowych. Przyjmijmy, że SN (z) oznacza liczbę naturalną kodu- jącą znak z. O tej funkcji zakładamy, że jest różnowartościowa i przyjmuje wartości parzyste wtedy i tylko wtedy, gdy argumentem jest zmienna.
Ustalenie sposobu kodowania znaków umożliwia kodowanie termów i formuł.
Dla termu t i formuły ϕ symbolami dte i dϕe będziemy oznaczać liczbę kodującą odpowiednio ten term i tę formułe. Niech
dte =
hSN (t)i jeżeli t jest zmienną lub stałą, hSN (+), dt1e , dt2ei jeżeli t = t1+ t2,
hSN (·), dt1e , dt2ei jeżeli t = t1· t2.
Liczbę dϕe kodującą daną formułę ϕ definiujemy analogicznym wzorem.
dϕe =
hSN (<), dt1e , dt2ei jeżeli ϕ = (t1 < t2) (podobnie dla ϕ = (t1 = t2)), hSN (∨), dψ1e , dψ2ei jeżeli ϕ = ψ1∨ ψ2,
hSN (¬), dψei jeżeli ϕ = ¬ψ, hSN (∃), dxe , dψei jeżeli ϕ = ∃ xψ
(i ewentualnie analogicznie dla koniunkcji i formuł ogólnych).
Lemat 1.8 Relacje
T erm(a) ⇔ a = dte dla pewnego termu t oraz
F orm(a) ⇔ a = dϕe dla pewnej formuły ϕ
są pierwotnie rekurencyjne. Istnieje też pierwotnie rekurencyjna funkcja Sub taka, że
Sub(dϕe , SN (x), dte) = dϕ[x ← t]e dla wszystkich formuł ϕ, zmiennych x i termów t.
Teraz powinniśmy ustalić pewien system logiczny. Przyjmijmy, że będziemy zajmować się systemem z książki Shoenfielda. Niech ϕ1, . . . , ϕnbędzie dowodem w tym systemie. Kodem tego dowodu będziemy nazywać liczbę
hdϕ1e , . . . , dϕnei.
Lemat 1.9 Załóżmy, że zbiór aksjomatów teorii T jest pierwotnie rekurencyjny.
Wtedy relacja
PrfT(a, b) ⇔ b koduje pewną formuła i a koduje jej dowód w teorii T
też jest pierwotnie rekurencyjna. Ponadto, jeżeli zbiór aksjomatów T jest rekuren- cyjny, to relacja PrfT jest rekurencyjna, a jeżeli jest rekurencyjnie przeliczalny, to taka jest też relacja PrfT.
1.4 Oryginalny dowód twierdzenie G¨ odla
1.4.1 ω-niesprzeczność i reprezentowalność
Teoria T (w języku arytmetyki) jest ω-niesprzeczna, jeżeli zawsze w sytuacji, gdy T ` ϕ[x ← n] dla wszystkich liczb n ∈ N , w T nie można dowieść formuły ∃x¬ϕ.
Teoria Q i arytmetyka Peano, a nawet wszystkie teorie, których aksjomaty są spełnione w naturalnym modelu arytmetyki N są ω-niesprzeczne.
Gdyby bowiem T było taką teorią i dała się w niej dowieść formuła ∃x¬ϕ, to ta formuła byłaby spełniona w modelu N . Wtedy także w tym modelu byłaby spełniona formuła ¬ϕ przy pewnym wartościowaniu h0. W modelu standardowym każdy element n uniwersum jest wartością termu stałego n. Mamy więc h0(x) = n[h0] dla pewnej liczby naturalnej n oraz N |= ¬ϕ[h0]. Z lematu zamieszczonego w części II dla h = h0 otrzymujemy, że N |= ¬ϕ[x ← n][h0]. Jest to jednak sprzeczne z założeniem, że N |= ¬ϕ[x ← n] (a więc dla dowolnego wartościowania, także dla h0).
Nietrudno zauważyć, że teorie ω-niesprzeczne są niesprzeczne.
Głównym powodem korzystania z ω-niesprzeczności jest możliwość łatwego uzasadnienia następującego lematu:
Lemat 1.10 Jeżeli T jest ω-niesprzecznym rozszerzeniem Q, to każda rekurencyj- nie przeliczalna relacja jest reprezentowalna w T .
Dowód. Niech S będzie relacją rekurencyjnie przeliczalną. Jako taka spełnia ona równoważność
S(m) ⇔ ∃n R(m, n)
dla pewnej rekurencyjnej relacji R. Przyjmijmy, że R jest mocno reprezentowalna przez w teorii T przez ϕ. Mamy więc
R(m, n) ⇒ T ` ϕ[x ← m][y ← n]
oraz
¬R(m, n) ⇒ T ` ¬ϕ[x ← m][y ← n].
Pokażemy, że relacja S jest reprezentowana w T przez formułę ∃y ϕ, a więc dla wszystkich m mamy
S(m) ⇔ T ` ∃y ϕ[x ← m].
Zauważmy, że
S(m) ⇒ R(m, n) dla pewnego n ⇒ T ` ϕ[x ← m][y ← n] dla pewnego n ⇒
⇒ T ` ∃y ϕ[x ← m].
Odwrotną implikację dowodzimy przez kontrapozycję. Jeżeli nie zachodzi S(m), to także dla żadnego n nie zachodzi R(m, n). Stąd dla wszystkich n mamy T `
¬ϕ[x ← m][y ← n]. Ponieważ T jest ω-niesprzeczna, więc w teorii T nie daje się dowieść ∃y ϕ[x ← m].2
Powyższy lemat pozostaje prawdziwy dla teorii niesprzecznych. Wtedy jednak jego dowód jest bardziej skomlikowany. Poza tym, G¨odel w swojej pracy zadowolił się założeniem ω-niesprzeczności, a wspomniane wzmocnienie lematu jest wyni- kiem późniejszym.
1.4.2 Sformułowanie twierdzenia
Twierdzenie 1.11 (G¨odel) Przypuśćmy, że T jest aksjomatyzowalną teorią za- pisaną w języku arytmetyki, zawierającą arytmetykę Q. Jeżeli teoria T jest ω- niesprzeczna, to jest niezupełna.
Dowód. Założenie o ω-niesprzeczności T w twierdzeniu G¨odla można osłabić do niesprzeczności. Przedstawimy teraz wersję orginalnego dowodu G¨odla korzystają- cą jednak z ω-niesprzeczności oraz z lematu przekątniowego z następnego rozdziału.
1.4.3 Lemat przekątniowy
Lemat 1.12 Przyjmijmy, że U ⊆ N2 oraz Ua = {b ∈ N : (a, b) ∈ U }. Wtedy zbiór P = {a ∈ N : (a, a) 6∈ U } jest różny od wszystkich zbiorów postaci Ua. Co więcej, zbiory te różnią się elementem a.
Dowód. Zbiory P i Uaróżnią się elementem a. W przeciwnym razie, albo a należy do obu tych zbiorów, albo do obu nie należy. Gdyby a ∈ P i a ∈ Ua, to z definicji tych zbiorów mielibyśmy, że ha, ai 6∈ U i odpowiednio ha, ai ∈ U , co nie jest moż- liwe. Gdyby a 6∈ P i a 6∈ Ua, to podobnie mielibyśmy, że ha, ai ∈ U i odpowiednio ha, ai 6∈ U , i to też nie jest możliwe. 2
Kilka uwag dotyczących lematu przekątniowego znajduje si rozdziale 1.3 części poświęconej formalizacji logiki.
1.4.4 Ważny zbiór U
W dowodzie G¨odla lemat przekątniowy stosujemy dla zbioru U = {(a, b) ∈ N2 : ∃ϕ ∈ F0 a = dϕe ∧ T ` ϕ[x ← b]},
gdzie x jest ustaloną zmienną, a F0 oznacza zbiór formuł, w których najwyżej x jest zmienną wolną. Zbiór ten można zdefiniować także następującymi wzorami
U = {(a, b) ∈ N2 : ∃ϕ ∈ F0 a = dϕe ∧ ∃y ∈ N PrfT(y, dϕ[x ← b]e)},
U = {(a, b) ∈ N2 : ∃ϕ ∈ F0 a = dϕe ∧ ∃y ∈ N PrfT(y, Sub(dϕe , SN (x), dbe))}
oraz
U = {(a, b) ∈ N2 : F orm0(a) ∧ ∃y ∈ N PrfT(y, Sub(a, SN (x), dbe))}
gdzie F orm0 jest arytmetyczną relacją odpowiadającą zbiorowi F0.
Korzystając z lematów 1.8 i 1.9, a także podobnych rozumowań otrzymujemy Wniosek 1.13 Relacja U jest rekurencyjnie przeliczalna dla wszystkich aksjoma- tyzowalnych teorii T . 2
1.4.5 Ciąg dalszy dowodu
Dla takiego zbioru U , zbiór P z lematu przekątniowego definiujemy wzorem P = {a ∈ N : ¬(F orm0(a) ∧ ∃y ∈ N PrfT(y, Sub(a, SN (x), dbe))}.
Tak więc
P = {a ∈ N : ∀y ∈ N ¬(F orm0(a) ∧ PrfT(y, Sub(a, SN (x), dbe))}.
Jeżeli przyjmiemy, że
R(a, y) ⇔ F orm(a) ∧ PrfT(y, Sub(a, SN (x), dae), to mamy
P = {a ∈ N : ∀y ∈ N ¬R(a, y)}.
Dowód przekątniowy jest zwykle dowodem nie wprost i polega na wykazaniu, że zbiór P jest jednym ze zbiorów Ua. W ten sposób uzyskujemy sprzeczność z lematem przekątniowym świadczącą o fałszywość przyjętych założeń, łącznie z założeniem dowodu nie wprost.
Zbiór U został zdefiniowany jako zbiór tych liczb, o których coś tam można dowieść w teorii T . Jeżeli naszym celem jest pokazanie równości P = Ua, to musi- my znaleźć analogiczną definicję zbioru P . Jest to możliwe dzięki rekurencyjności relacji R i reprezentowalności takich relacji.
Weźmy więc formułę φ reprezentującą w teorii T relację R. Tak więc R(a, y) ⇒ T ` φ[x ← a][z ← y]
oraz
¬R(a, y) ⇒ T ` ¬φ[x ← a][z ← y].
Jeżeli reprezentujemy w teoriach niesprzecznych, to podane implikacje można za- stąpić równoważnościami. W szczególności mamy więc, że
¬R(a, y) ⇔ T ` ¬φ[x ← a][z ← y]
i zbiór P można zdefiniować także w następujący sposób
P = {a ∈ N : ∀y ∈ N T ` ¬φ[x ← a][z ← y]}.
Chcielibyśmy jednak zdefiniować go w postaci P = {a ∈ N : T ` ψ[x ← a]}
dla pewnej formuły ψ. Gdyby nam to się udało, to byłaby prawdziwa równość P = Udψe i uzyskalibyśmy sprzeczność. Musimy więc znaleźć kandydata na ψ i dowieść odpowiednią równoważność.
Nietrudno zauważyć, że analizując P możemy skorzystać z ω-niesprzeczności T . Załóżmy, że a ∈ P . Założenie o ω-niesprzeczności implikuje, że w teorii T nie daje się dowieść formuła ∃z φ[x ← a]. Ta formuła jest zdaniem, więc z zupełności teorii T (czyli założenia dowodu nie wprost) wynika, że
T ` ¬∃z φ[x ← a], a korzystając z praw de Morgana otrzymujemy, że T ` ∀z ¬φ[x ← a].
Zauważmy na koniec, że ten ostatni fakt może zostać wyrażony jako stwierdzenie a ∈ Ud∀z ¬φe. Tym samym dowiedliśmy zawieranie P ⊆ Ud∀z ¬φe.
Zawieranie odwrotne
Ud∀z ¬φe ⊆ P (1)
też zachodzi. Co więcej, to zawieranie jest oczywiste, nie wymaga żadnych specjal- nych założeń i wynika z zasad logiki.
Zachodzi więc równość P = Ud∀z ¬φe. Z wcześniejszej analizy wiemy jednak, że ta równość prowadzi do sprzeczności. Tak więc teoria T jest niezupełna. Twiedzenie G¨odla zostało więc dowiedzione, ale bez wskazania formuły, której nie da się ani dowieść, ani obalić.
1.5 Dodatkowy wniosek
Wniosek 1.14 (G¨odel) Przypuśćmy, że T jest aksjomatyzowalną teorią zapisaną w języku arytmetyki, zawierającą arytmetykę Q. Jeżeli teoria T jest ω-niesprzeczna, to istnieje taka formuła ψ z jedną zmienną wolną z, że
T ` ψ[z ← n]
dla wszystkich liczb naturalnych n, dla której jednak T 6` ∀z ψ.
Dowód. Z dowodu twierdzenia G¨odla wiemy, że zachodzi zawieranie (1) Ud∀z ¬φe ⊆ P.
Z lematu przekątniowego wynika, że te zbiory różnią się elementem m = d∀z ¬φe.
Wobec tego, m ∈ P , ale m 6∈ Ud∀z ¬φe. Stąd otrzymujemy odpowiednio, że
∀y ∈ N T ` ¬φ[x ← m][z ← y] oraz T 6` ∀z ¬φ[x ← m].
Aby otrzymać tezę wystarczy przyjąć, że
ψ = ¬φ[x ← m] = ¬φ[x ← d∀z ¬φe]. 2
Wniosek 1.15 (G¨odel) Przypuśćmy, że T jest aksjomatyzowalną teorią zapisaną w języku arytmetyki, zawierającą arytmetykę Q. Jeżeli teoria T jest ω-niesprzeczna, to jest niezupełna.
Dowód. Korzystając z założenia o ω-niesprzeczności i poprzedniego wniosku bez trudu pokazujemy, że w teorii T nie można ani dowieść, ani obalić zdania ∀z ψ.
W ten sposób dowiedliśmy twierdzenie G¨odla o niezupełności podając zdanie nie- zależne od T . 2
2 Twierdzenie G¨ odla według Churcha
2.1 Teza Churcha
Dawid Hilbert uważał za konieczne po uporządkowaniu spraw związanych z pod- stawami matematyki zajęcie się tzw. Entscheidungsproblem-em1, którego rozwią- zanie wymagało opracowania skończonej procedury umożliwiającej stwierdzenie, czy dana formuła jest prawem rachunku kwantyfikatorów.
1The Entscheidungsproblem is solved when one knows a procedure by which one can decide in a finite number of operations whether a given logical expression is generally valid or is satisfiable.
The solution of the Entscheidungsproblem is of fundamental importance for the theory of all fields, the theorems of which are at all capable of logical development from finitely many axioms.
D. Hilbert, W. Ackermann, Grundz¨uge der theoretischen Logik, 1928.
Alonzo Church brał pod uwagę możliwość negatywnego rozwiązania tego pro- blemu. Wymagało to precyzyjnego określenia tych problemów, które dają się roz- wiązać za pomocą dowolnie rozumianych skończonych procedur. Dzisiaj takie pro- blemy nazywa się obliczalnymi lub efektywnie obliczalnymi. Mówimy też o funk- cjach obliczalnych. Przykładami skończonych procedur są też programu kompute- rowe, zwłaszcza zawsze kończące obliczenia. Przykładami obliczalnych problemów i funkcji są w szczególności te, które potrafimy rozwiązywać bądź obliczać za po- mocą komputerów.
Około 1932 roku Alonzo Church doszedł do wniosku, że obliczalność da się sformalizować za pomocą λ-rachunku. Od tego momentu szukał argumentów uza- sadniających swoje przekonania. Podpowiedział2 mu je Kurt G¨odel podczas wy- kładu wygłoszonego w Princeton wiosną 1934 roku. G¨odel najpierw zauważył, że funkcje pierwotnie rekurencyjne są obliczalne za pomocą skończonych procedur i powiedział, że wie, jak rozszerzyć definicję rekurencyjności, aby zachodziło też stwierdzenie odwrotne. Następnie zaproponował definicję funkcji rekurencyjnych, określanych jako funkcje rekurencyjne według Herbranda i G¨odla. Definicja ta szybko została przekształcona w przytoczoną w tych materiałach definicję reku- rencyjności. Stephen Kleene przy pewnym udziale Churcha dowiódł równoważność rekurencyjności i λ-obliczalności. Twierdzenie to stało się głównym argumentem za słusznością tezy Churcha.
W 1936 roku Church sformułował i zaproponował przyjęcie tzw. tezy Chur- cha. Zgodnie z nią pojęcie funkcji rekurencyjnej i równoważne mu pojęcie λ- obliczalności stanowią dobre formalizacje pojęcia obliczalności. W szczególności, zgodnie z tą tezą każda funkcja naturalna, której wartości potrafimy efektywnie obliczać w jakimkolwiek sensie, powinna być rekurencyjna. W konsekwencji powin- niśmy uznać, że problemy rozstrzygalne rozumiane jako zbiory liczb naturalnych to dokładnie zbiory rekurencyjne, a problemy semirozstrzygalne (rozpoznawalne) to zbiory rekurencyjnie przeliczalne.
Swoją tezę Church uzasadniał równoważnością pojęcia λ-obliczalności i reku- rencyjności. Uważał, że równoważność dwóch prób formalizacji obliczalności mo- tywowanych w bardzo różny sposób nie jest przypadkowa.
W tym samym czasie i niezależnie analogiczną tezę sformułował Alan Turing.
Twierdził on, że wszystkie naturalne funkcje obliczalne mogą być obliczane na maszynach Turinga. Tezę tę Turing uzasadniał w inaczej niż Church. Uważał, że maszyny Turinga bardzo dobrze opisują sposóby liczenia stosowane przez ludzi, a nawet mogą opisywać działanie mózgu (uważał, że mózg można uważać za skończo- ną, wielostanową maszynę). Jeżeli ludzie liczą tak, jak maszyny Turinga, to wszel- kie funkcje obliczane jakkolwiek przez ludzi muszą dawać się obliczać za pomocą maszyn Turinga. W związku tym czasem mówi się też o tezie Turinga-Churcha, a nawet samego Turinga.
Turing wzmocnił też argumentację Churcha dowodząc twierdzenie o równoważ- ności obliczalności na maszynach Turinga i λ-obliczalności.
Kurt G¨odel do końca życia zaprzeczał, że wygłaszając podczas wykładu w Prin- ceton swoją opinię myślał o czymś przypominającym tezę Churcha. Nie wykluczo- ne, że przewidywał tylko możliwość jakiegoś sformalizowania „obliczeń skończo- nych” i wykazania, że pozwalają na obliczanie dokładnie funkcji rekurencyjnych.
2(Primitive) recursive functions have the important property that, for given set of values of the arguments, the value of the function can be computed by finite procedure. I w dopisku: The convers seems to be true if, besides recursions according to the (primitive recursion) scheme (2), recursion of other forms (e.g. with respect to two variables simultaneously) are admitted.
2.2 Twierdzenie o nierozstrzygalności arytmetyki
Przyjmijmy, że T oznacza niesprzeczną teorię zapisaną w języku arytmetyki i za- wierającą arytmetykę Q. Niech U będzie zbiorem z dowodu twierdzenia G¨odla:
U = {(a, b) ∈ N2 : ∃ϕ ∈ F a = dϕe ∧ T ` ϕ[x ← b]}.
Twierdzenie 2.1 (Church) Jeżeli T jest niesprzeczną aksjomatyzowalną teorią zapisaną w języku arytmetyki i zawierającą arytmetykę Q, to zbiór U jest rekuren- cyjnie przeliczalny i nie jest rekurencyjny.
Dowód. Rekurencyjna przeliczalność U jest oczywista. Sprowadzimy więc do sprzeczności założenie, że U jest rekurencyjny.
Jak zwykle przyjmujemy, że P = {b ∈ N : (b, b) 6∈ U }. Jeżeli U jest reku- rencyjny, to także P jest rekurencyjny i mocno reprezentowalny w T . Załóżmy, że ϕ mocno reprezentuje P . Ponieważ P jest mocno reprezentowalny w teorii nie- sprzecznej, więc
b ∈ P ⇐⇒ T ` ϕ[x ← b].
Stąd wynika, że
P = {b ∈ N : T ` ϕ[x ← b]} = {b ∈ N : (dϕe , b) ∈ U } = Udϕe. Z lematu przekątniowego wiemy jednak, że nie jest to możliwe. 2
Wniosek 2.2 Jeżeli T jest niesprzeczną teorią aksjomatyzowalną zapisaną w ję- zyku arytmetyki i zawierającą arytmetykę Q, to
{a ∈ N : ∃ϕ ∈ F a = dϕe ∧ ϕ jest zdaniem ∧ T ` ϕ}
oraz
{a ∈ N : ∃ϕ ∈ F a = dϕe ∧ T ` ϕ}
nie są rekurencyjne. W szczególności zbiory twierdzeń arytmetyki Q i arytmetyki Peano nie są rekurencyjne.
Dowód. Jeżeli drugi z tych zbiorów oznaczymy symbolem X i przyjmiemy, że jest rekurencyjny, to dzięki równoważności
(a, b) ∈ U ⇐⇒ Sub(a, SN (x), dbe) ∈ X pokażemy, że U jest rekurencyjny. To jednak nie jest możliwe. 2
2.3 Entscheidungsproblem
Twierdzenie 2.3 (Church) Zbiór praw rachunku kwantyfikatorów (zarówno z równością, jak i bez równości) jest rekurencyjnie przeliczalny i nie jest rekuren- cyjny.
2.4 Twierdzenie o niezupełności arytmetyki
Lemat 2.4 Jeżeli T jest teorią niesprzeczną, zupełną i aksjomatyzowalną, to
{a ∈ N : ∃ϕ ∈ F a = dϕe ∧ ϕ jest zdaniem ∧ T ` ϕ}
jest rozstrzygalny.
Dowód. Niech A będzie zbiorem z tezy lematu i niech
B = {a ∈ N : ∃ϕ ∈ F a = dϕe ∧ ϕ jest zdaniem ∧ T ` ¬ϕ}.
Oba te zbiory są rekurencyjnie przeliczalne. Mamy więc
a ∈ A ⇔ ∃n R(a, n) oraz a ∈ B ⇔ ∃n S(a, n)
dla pewnych rekurencyjnych relacji R i S. Niech f będzie funkcją rekurencyjną taką, że
f (a) = µn (R(a, n) ∨ S(a, n) ∨ ¬(F orm(a) ∧ n = 0)).
Zupełność T implikuje, że jest to funkcja całkowita (F orm(a) powinno oznaczać, że a jest numerem zdania). Zauważmy, że
a ∈ A ⇐⇒ R(a, f (a)), a to oznacza, że A jest relacją rekurencyjną.2
Wniosek 2.5 (twierdzenie G¨odla o niezupełności) Jeżeli T jest zapisaną w języku arytmetyki i zawierającą arytmetykę Q teorią niesprzeczną i aksjomatyzo- walną, to T nie jest zupełna. 2
