Logika dla informatyków/Arytmentyka pierwszego rzędu: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
m
 
(Nie pokazano 8 wersji utworzonych przez 2 użytkowników)
Linia 1: Linia 1:
Słowo ''arytmetyka'' używane jest w odniesieniu do różnych teorii dotyczących liczb naturalnych. Nasza sygnatura dla arytmetyki pierwszego rzędu składa się z dwuargumentowych symboli funkcyjnych <math>+</math> i <math>\cdot\,</math>, oznaczających dodawanie i mnożenie,symbolu następnika s, oraz stałej 0.  
+
Słowo ''arytmetyka'' używane jest w odniesieniu do różnych teorii dotyczących liczb naturalnych. Nasza sygnatura dla arytmetyki pierwszego rzędu składa się z dwuargumentowych symboli funkcyjnych <math>+</math> i <math>\cdot\,</math>, oznaczających dodawanie i mnożenie, symbolu następnika s oraz stałej 0.  
  
Skoro przedmiotem arytmetyki są liczby naturalne, więc strukturę <math>\mathfrak N = <\mathbb N, +,\cdot, 0, \su></math>, ze "zwykłymi" operacjami arytmetycznymi nazwiemy ''standardowym modelem arytmetyki''.Zbiór <math>Th(\mathfrak N)</math> złożony ze wszystkich zdań prawdziwych w&nbsp;modelu <math>\mathfrak N</math> nazywiemy zaś ''arytmetyką zupełną''. Niestety,arytmetyka zupełna nie wyznacza modelu standardowego jednoznacznie.
+
Skoro przedmiotem arytmetyki są liczby naturalne, strukturę <math>\mathfrak N = <\mathbb N, +,\cdot, 0, \su></math> ze "zwykłymi" operacjami arytmetycznymi nazwiemy ''standardowym modelem arytmetyki''. Zbiór <math>Th(\mathfrak N)</math> złożony ze wszystkich zdań prawdziwych w&nbsp;modelu <math>\mathfrak N</math> nazywiemy zaś ''arytmetyką zupełną''. Niestety,arytmetyka zupełna nie wyznacza modelu standardowego jednoznacznie.
  
 
{{fakt|9.1|ranny|
 
{{fakt|9.1|ranny|
Linia 9: Linia 9:
 
<center><math>\mathfrak M = <\mathbb M, \oplus,\otimes, 0, S></math>, </center>
 
<center><math>\mathfrak M = <\mathbb M, \oplus,\otimes, 0, S></math>, </center>
  
która jest  elementarnie równoważna&nbsp;<math>\mathfrak N</math> ale nieizomorficzna z&nbsp;<math>\mathfrak N</math>.}}
+
która jest  elementarnie równoważna&nbsp;<math>\mathfrak N</math>, ale nieizomorficzna z&nbsp;<math>\mathfrak N</math>.}}
  
  
 
{{dowod|||
 
{{dowod|||
  
Niech <math>\Delta</math> składa się ze wszystkich formuł postaci <math>x\not=s(s(\ldots s(0)\ldots))</math>.Nietrudno pokazać, że każdy skończony podzbiór zbioru<math> Th(\mathfrak N)\cup\Delta</math> jest spełnialny w&nbsp;modelu&nbsp;<math>\mathfrak N</math> przez dostatecznie dużą wartość <math>x</math>. Na mocy twierdzenia o zwartości ([[Logika dla informatyków/Teoria modeli#qqryq|Twierdzenie 8.1]]),całość jest spełnialna w pewnym modelu&nbsp;<math>\mathfrak M</math> przez pewne wartościowanie <math>\varrho</math>. Wtedy <math>\mathfrak M</math> spełnia te same zdania co <math>\mathfrak N</math>, aleelement <math>\varrho(x)</math> nie ma odpowiednika w modelu <math>\mathfrak N</math>, bo każdy element <math>\mathfrak N</math> można otrzymać z zera za pomocą nastepnika.Z&nbsp;[[Logika dla informatyków/Teoria modeli#ryqqq|Twierdzenia 8.2]] wynika, że model&nbsp;<math>\mathfrak M</math> może być żądanej mocy.
+
Niech <math>\Delta</math> składa się ze wszystkich formuł postaci <math>x\not=s(s(\ldots s(0)\ldots))</math>. Nietrudno pokazać, że każdy skończony podzbiór zbioru <math> Th(\mathfrak N)\cup\Delta</math> jest spełnialny w&nbsp;modelu&nbsp;<math>\mathfrak N</math> przez dostatecznie dużą wartość <math>x</math>. Na mocy twierdzenia o zwartości ([[Logika dla informatyków/Teoria modeli#qqryq|Twierdzenie 8.1]]), całość jest spełnialna w pewnym modelu&nbsp;<math>\mathfrak M</math> przez pewne wartościowanie <math>\varrho</math>. Wtedy <math>\mathfrak M</math> spełnia te same zdania co <math>\mathfrak N</math>, ale element <math>\varrho(x)</math> nie ma odpowiednika w modelu <math>\mathfrak N</math>, bo każdy element <math>\mathfrak N</math> można otrzymać z zera za pomocą nastepnika. Z&nbsp;[[Logika dla informatyków/Teoria modeli#ryqqq|Twierdzenia 8.2]] wynika, że model&nbsp;<math>\mathfrak M</math> może być żądanej mocy.
 
}}
 
}}
  
Linia 21: Linia 21:
 
{{twierdzenie|9.2 (Gödel)|godel|
 
{{twierdzenie|9.2 (Gödel)|godel|
  
Dla dowolnej częściowej funkcji obliczalnej <math>f:\mathbb N^k\rightarrow\mathbb N</math> istnieje taka formuła <math>\var\varphi</math>, że <math>FV(\var\varphi)\subseteq\{x_1,\ldots,x_k,y\}</math> oraz dla <math>\varrho(x_1)=n_1,\ldots,\varrho(x_k)=n_k,\varrho(y)=m</math> zachodzi równoważność  
+
Dla dowolnej częściowej funkcji obliczalnej <math>f:\mathbb N^k\rightarrow\mathbb N</math> istnieje taka formuła <math>\var\varphi</math>, że <math>FV(\var\varphi)\subseteq\{x_1,\ldots,x_k,y\}</math> oraz dla <math>\varrho(x_1)=n_1,\ldots,\varrho(x_k)=n_k,\varrho(y)=m</math> zachodzi równoważność  
  
<center> <math>(\mathfrak N,\varrho)\models\var\varphi</math> wtedy i tylko wtedy, gdyd <math>f(n_1,\ldots,n_k)=m</math>. </center>
+
<center> <math>(\mathfrak N,\varrho)\models\var\varphi</math> wtedy i tylko wtedy, gdy <math>f(n_1,\ldots,n_k)=m</math>. </center>
 
}}
 
}}
  
Linia 35: Linia 35:
 
{{dowod|||
 
{{dowod|||
  
Z [[#expr|Twierdzenia 9.2]] wynika w szczególności, że dla dowolnego zbioru rekurencyjnie przeliczalnego <math>A\subseteq\NN</math> istnieje formuła <math>\var\varphi(x)</math>,o jednej zmiennej wolnej&nbsp;<math>x</math>, dla której
+
Z [[#expr|Twierdzenia 9.2]] wynika w szczególności, że dla dowolnego zbioru rekurencyjnie przeliczalnego <math>A\subseteq\NN</math> istnieje formuła <math>\var\varphi(x)</math>, o jednej zmiennej wolnej&nbsp;<math>x</math>, dla której
  
 
<center> <math>(\mathfrak N,x:n)\models\var\varphi</math>wtedy i tylko wtedy, gdy  <math>n\in A</math>. </center>
 
<center> <math>(\mathfrak N,x:n)\models\var\varphi</math>wtedy i tylko wtedy, gdy  <math>n\in A</math>. </center>
Linia 41: Linia 41:
 
Korzystając z [[Logika dla informatyków/Język logiki pierwszego rzędu#lem-pier-1|Lematu 2.10]], możemy napisać to tak:
 
Korzystając z [[Logika dla informatyków/Język logiki pierwszego rzędu#lem-pier-1|Lematu 2.10]], możemy napisać to tak:
  
<center><math>\var\varphi(\underline n)\in Th(\mathfrak N)</math> wtedy i tylko wtedy , gdy  <math>n\in A</math>,</center>
+
<center><math>\var\varphi(\underline n)\in Th(\mathfrak N)</math> wtedy i tylko wtedy, gdy  <math>n\in A</math>,</center>
  
 
gdzie symbol <math>\underline n</math> oznacza term <math>s^n(0)</math>. A więc rozstrzygalność <math>Th(\mathfrak N)</math> implikowałaby rozstrzygalność problemu stopu.  
 
gdzie symbol <math>\underline n</math> oznacza term <math>s^n(0)</math>. A więc rozstrzygalność <math>Th(\mathfrak N)</math> implikowałaby rozstrzygalność problemu stopu.  
  
Abyudowodnić drugą część twierdzenia, przypomnijmy, że problem decyzyjny
+
Aby udowodnić drugą część twierdzenia, przypomnijmy, że problem decyzyjny
  
<center>''Czy dana maszyna Turinga zatrzymuje się dla każdego słowawejściowego?''</center>
+
<center>''Czy dana maszyna Turinga zatrzymuje się dla każdego słowa wejściowego?''</center>
  
nie jest częściowo rozstrzygalny, i że to samo dotyczy jego dopełnienia. Jeśli zakodujemy nasz problem w postaci zbioru <math>A\subseteq\mathbb N</math>, to zbiórten będzie można zdefiniować formułą arytmetyki z dwoma kwantyfikatorami,wyrażającą własność
+
nie jest częściowo rozstrzygalny, i że to samo dotyczy jego dopełnienia. Jeśli zakodujemy nasz problem w postaci zbioru <math>A\subseteq\mathbb N</math>, to zbiór ten będzie można zdefiniować formułą arytmetyki z dwoma kwantyfikatorami, wyrażającą własność
  
<center> Dla każdego ''(kodu) słowa <math>w</math> ''istnieje'' kod obliczenia akceptującego to słowo.''
+
<center> Dla każdego ''(kodu) słowa <math>w</math> ''istnieje'' kod obliczenia akceptującego to słowo.''</center>
  
 
Zbiór <math>A</math> jest więc też definiowalny formułą arytmetyki i byłby rekurencyjnie przeliczalny, gdyby taka była teoria <math>Th(\mathfrak N)</math>.
 
Zbiór <math>A</math> jest więc też definiowalny formułą arytmetyki i byłby rekurencyjnie przeliczalny, gdyby taka była teoria <math>Th(\mathfrak N)</math>.
Linia 57: Linia 57:
  
 
===Twierdzenie Gödla o niezupełności ===
 
===Twierdzenie Gödla o niezupełności ===
Skoro nie można zdefiniować jednoznacznie modelu standardowego(Fakt&nbsp;[[#ranny]]), może można chociaż, za pomocą odpowiednich aksjomatów,scharakteryzować zdania które są w nim prawdziwe?Przez&nbsp;PA (od ,,Peano Arithmetics'') oznaczymy teorię o aksjomatach:
+
Skoro nie można zdefiniować jednoznacznie modelu standardowego([[#ranny|Fakt 9.1]]), może można chociaż, za pomocą odpowiednich aksjomatów, scharakteryzować zdania które są w nim prawdziwe? Przez&nbsp;PA (od "Peano Arithmetics") oznaczymy teorię o aksjomatach:
  
 +
*<math>\forall x\forall y\,(s(x)=s(y)\to x=y)</math>;
 +
*<math>\forall x\neg (s(x)=0)</math>
 +
*<math>\forall x\ (x+0 = x)</math>;
 +
*<math>\forall x\forall y\ (x+s(y) = s(x+y))</math>;
 +
*<math>\forall x (x\cdot 0 = 0)</math>;
 +
*<math>\forall x\forall y\ (x\cdot s(y) = (x\cdot y)+x)</math>;
 +
*<math>\forall x (\var\varphi(x)\to\var\varphi(s(x)))\to(\var\varphi(0)\to\forall x\,\var\varphi(x))</math>,
  
*<math>\forall x\forall y\,(\su(x)=\su(y)\to x=y)</math>;
+
gdzie <math>\var\varphi(x)</math> może być dowolną formułą. Pierwsze dwa aksjomaty mówią, że operacja następnika jest różnowartościowa, a zero nie jest następnikiem żadnej liczby  (to gwarantuje nieskończoność każdego modelu). Kolejne dwa aksjomaty stanowią indukcyjną definicję dodawania, a&nbsp;następne dwa --- indukcyjną definicję mnożenia. Na końcu zamiast pojedynczego aksjomatu, mamy schemat aksjomatu, nazywany schematem ''indukcji''. Zatem zbiór aksjomatów Peano jest w istocie nieskończony. Ale zbiór ten jest rekurencyjny: można efektywnie ustalić co jest aksjomatem, a co nie jest.  
*<math>\forall x\neg (\su(x)=0)</math>
 
*<math>\forall x\,(x+0 = x)</math>;
 
*<math>\forall x\forall y\,(x+\su(y) = \su(x+y))</math>;
 
*<math>\forall x\,(x\cdot 0 = 0)</math>;
 
*<math>\forall x\forall y\,(x\cdot\su(y) = (x\cdot y)+x)</math>;
 
*</math>\forall x\,(\var\varphi(x)\to\var\varphi(\su(x)))\to(\var\varphi(0)\to\forall x\,\var\varphi(x)</math>),
 
<!--%-->gdzie <math>\var\varphi(x)</math> może być dowolną formułą. Pierwsze dwa aksjomaty mówią, że operacja następnika jest różnowartościowa, a zero nie jest następnikiem żadnej liczby  (to gwarantujenieskończoność każdego modelu). Kolejne dwa aksjomaty stanowią indukcyjnądefinicję dodawania, a&nbsp;następne dwa --- indukcyjnądefinicję mnożenia. Na końcu zamiast pojedynczego aksjomatu, mamy schemat aksjomatu, nazywany schematem ''indukcji''. Zatem zbiór aksjomatów Peano jest w istocie nieskończony. Ale zbiór ten jest rekurencyjny: możnaefektywnieustalić co jest aksjomatem a co nie jest.  
 
  
Oczywiście standardowy model arytmetyki jest modelem arytmetyki Peano:<!--%--><center><math>\mathfrak N\models {\rm PA}.</math></center><!--%-->Inaczej mówiąc, wszystkie konsekwencje aksjomatów Peano (twierdzeniateorii&nbsp;PA) są prawdziwe w standardowym modelu. A na odwrót? Kiedyś przypuszczano, że PA jest ''teorią zupełną'' (por.&nbsp;Definicja&nbsp;[[#slmFOjof]]), tj. że każde zdanie prawdziwe w <math>\mathfrak N</math> jest twierdzeniem arytmetyki Peano.
+
Oczywiście standardowy model arytmetyki jest modelem arytmetyki Peano:<!--%--><center><math>\mathfrak N\models {\rm PA}.</math></center><!--%-->
 +
Inaczej mówiąc, wszystkie konsekwencje aksjomatów Peano (twierdzenia teorii&nbsp;PA) są prawdziwe w standardowym modelu. A na odwrót? Kiedyś przypuszczano, że PA jest ''teorią zupełną'' (por.&nbsp;[[Logika dla informatyków/Ograniczenia logiki pierwszego rzędu#slmFOjof|Definicja 4.14]]), tj. że każde zdanie prawdziwe w <math>\mathfrak N</math> jest twierdzeniem arytmetyki Peano.
  
<!--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%-->Przypuszczenie to okazało sie fałszywe dzieki odkryciu dokonanemu przez G\"odla, a mianowicie dzięki metodzie ''arytmetyzacji'' (numeracji G\"odla), która pozwoliła na wyrażanie w języku arytmetyki faktów odnoszącychsię do samej arytmetyki, w szczególności istnienia lub nieistnienia dowodu dla danej formuły.  
+
Przypuszczenie to okazało się fałszywe dzięki odkryciu dokonanemu przez Gödla, a mianowicie dzięki metodzie ''arytmetyzacji'' (numeracji Göodla), która pozwoliła na wyrażanie w języku arytmetyki faktów odnoszących się do samej arytmetyki, w szczególności istnienia lub nieistnienia dowodu dla danej formuły.  
  
{{twierdzenie||tgonzap|
+
{{twierdzenie|9.4 (Gödla o niezupełności|tgonzap|
  
 +
Istnieje takie zdanie <math>Z</math> w języku arytmetyki, że <math>{\rm PA}\not\vdash_H Z</math> i&nbsp;<math>{\rm PA}\not\vdash_H\neg Z</math>. }}
 +
 +
{{dowod|||
 +
 +
Skoro zbiór aksjomatów PA jest rekurencyjny, więc zbiór wszystkich twierdzeń teorii PA (formuł, które można wyprowadzić z tych aksjomatów) jest rekurencyjnie przeliczalny. Aby bowiem stwierdzić, że dana formuła jest twierdzeniem PA, wystarczy systematycznie generować wszystkie możliwe dowody, aż wreszcie otrzymamy ten właściwy.
  
 +
Gdyby PA była teorią zupełną, to dla dowolnego zdania <math>\var\varphi</math>, prędzej czy później znaleźlibyśmy albo dowód formuły <math>\var\varphi</math> albo formuły <math>\neg\var\varphi</math>. A więc w takim przypadku PA byłaby po prostu rozstrzygalna.
  
Istnieje takie zdanie <math>Z</math> w języku arytmetyki, że <math>{\rm PA}\not\vdash_H Z</math> i&nbsp;<math>{\rm PA}\not\vdash_H\neg Z</math>. }}
+
Ale z drugiej strony, teoria zupełna jest identyczna z teorią każdego swojego modelu, więc PA byłaby identyczna z <math>Th(\mathfrak N)</math>. Wówczas jednak teoria <math>Th(\mathfrak N)</math> musiałaby być rozstrzygalna, co przeczy [[#przescieradlo|Wnioskowi 9.3]].
 +
}}
 +
 
 +
Istota twierdzenia Gödla polega nie na tym, że akurat PA jest niezupełna. Jeśli zbiór aksjomatów PA rozszerzymy do innego (rekurencyjnie przeliczalnego) zbioru aksjomatów prawdziwych w <math>\mathfrak N</math>, to nadal będzie istniało zdanie niezależne od tych aksjomatów. Dowód pozostanie prawie bez zmian. A więc nie tylko PA, ale w ogóle każda efektywnie zadana teoria musi być niezupełna, jeśli tylko jest dostatecznie silna na to, aby dało sie w niej zinterpretować pojęcia arytmetyczne.
  
{{dowod||
+
Przytoczony powyżej "współczesny" dowód twierdzenia Gödla wykorzystuje numerację gödlowską pośrednio, poprzez odwołanie się do pojęcia rozstrzygalnego problemu decyzyjnego. (Mówiąc o algorytmach generujących dowody, w istocie mamy na myśli pewne obliczenia na kodach takich dowodów, itd.). Oryginalny dowód Göodla posługiwał się numeracją bezpośrednio i przebiegał mniej więcej tak jak niżej. Na początek numerujemy wszystkie symbole języka arytmetyki:
  
Skoro zbiór aksjomatów PA jest rekurencyjny, więc zbiór wszystkich twierdzeń teorii PA (formuł, które można wyprowadzić z tych aksjomatów)jest rekurencyjnie przeliczalny. Aby bowiem stwierdzić, że dana formuła jest twierdzeniem PA, wystarczy systematycznie generować wszystkie możliwe dowody, aż wreszcie otrzymamy ten właściwy.
+
{|style="width:75%;"
 +
|-
 +
!Symbol:
 +
|<math>0</math>||<math>s</math>|| <math>+</math>||<math>\cdot</math>||<math> \bot</math>||<math> \to </math>||<math>=</math>||<math> \forall\</math>||(||)||<math>x_0</math>||<math>x_1</math>|| <math>\dots</math>
 +
|-
 +
!Numer:
 +
|1||2||3||4||5||6||7||8||9||10||11||12||<math>\dots</math>
 +
|}
  
Gdyby PA była teorią zupełną, to dla dowolnego zdania <math>\var\varphi</math>, prędzej czy później znaleźlibyśmy albo dowód formuły <math>\var\varphi</math> albo formuły <math>\neg\var\varphi</math>. A więc w takim przypadku PA byłabypo prostu rozstrzygalna.
+
Każdemu ciągowi znaków, w tym każdej formule, dowodowi itp., można teraz przypisać kod liczbowy. Jeśli przez <math>\#a</math> oznaczymy numer znaku <math>a</math>, to kodem napisu "<math>a_1a_2\ldots a_n</math>" jest liczba <!--%-->
  
Ale z drugiej strony, teoria zupełna jest identyczna z teorią każdego swojego modelu, więc PA byłaby identyczna z <math>'''Th'''(\mathfrak N)</math>.Wówczas jednak teoria <math>'''Th'''(\mathfrak N)</math> musiałaby być rozstrzygalna, co przeczy Wnioskowi&nbsp;[[#przescieradlo]]. }}
+
<center><math>Kod (a_1a_2\ldots a_n) = 2^{\#a_1}3^{\#a_2}5^{\#a_3}7^{\#a_4\cdots} p_n^{\#a_n},</math></center>
  
Istota twierdzenia G\"odla polega nie na tym, że akurat PA jest niezupełna.Jeśli zbiór aksjomatów PA rozszerzymy do innego (rekurencyjnie przeliczalnego)zbioru aksjomatów prawdziwych w <math>\mathfrak N</math> to nadal będzie istniało zdanie niezależne od tych aksjomatów. Dowód pozostanie prawiebez zmian. A więc nie tylko PA, ale w ogóle każdaefektywnie zadana teoria musi być niezupełna, jeśli tylko jest dostatecznie silna na to, aby dało sie w niej zinterpretować pojęcia arytmetyczne.
+
<!--%-->gdzie <math>p_n</math> oznacza <math>n</math>-tą liczbę pierwszą. Odkrycie Gödla oparte jest na obserwacji, że własności formuł arytmetyki mogą być wyrażane w języku samej arytmetyki jako teorioliczbowe własności kodów. Zamiast np.&nbsp;mówić o własnościach formuły<math>\forall x_0((x_1+x_0=0)\to\bot)</math>, można mówić o własnościach jej kodu, tj. liczby <!--%-->
  
Przytoczony powyżej ,,współczesny'' dowód twierdzenia G\"odla wykorzystuje numerację g\"odlowską pośrednio, poprzez odwołanie się do pojęcia rozstrzygalnego problemu decyzyjnego. (Mówiąc o algorytmach generujących dowody, w istocie mamy na myśli pewne obliczenia na kodach takich dowodów, itd.) Oryginalny dowód G\"odla posługiwał się numeracją bezpośrednio i przebiegał mniej więcejtak jak niżej. Na początek numerujemy wszystkie symbole języka arytmetyki:
+
<center><math>Kod(\forall x_0((x_1+x_0=0)\to\bot)) =2^8 3^{11} 5^9 7^9 11^{12} 13^3 17^{11} 19^7 23^1 29^{10} 31^6 37^5 41^{10}.</math></center>
  
\begin{tabbing}Symbol: \=\quad <math>0</math>\quad \=\quad <math>\su</math>\quad \=\quad <math>+</math>\quad \=\quad <math>\cdot</math>\quad\=<math>\quad \bot</math>\quad\=<math>\quad \to\quad </math>\=<math>\quad =\quad</math>\=<math>\quad \forall\quad</math>\=\quad (\quad \=\quad\ )\quad \=<math>\quad x_0\quad </math>\=<math>\quad x_1\quad</math>\=\quad \dots\\Numer: \>\quad 1\>\quad 2\>\quad 3\>\quad 4\>\quad 5 \>\quad 6\>\quad 7\>\quad 8\>\quad 9\>\quad 10\>\quad 11\>\quad 12\>\quad\dots\end{tabbing}
 
  
Każdemu ciągowi znaków, w tym każdej formule, dowodowi itp.,można teraz przypisać kod liczbowy. Jeśli przez <math>\#a</math> oznaczymy numer znaku <math>a</math>, to kodem napisu ,,<math>a_1a_2\ldots a_n</math>'' jest liczba <!--%--></math></center>''Kod\/}(a_1a_2\ldots a_n) = 2^{\#a_1}3^{\#a_2}5^{\#a_3}7^{\#a_4''\cdotsp_n^{\#a_n},</math></center><!--%-->gdzie <math>p_n</math> oznacza <math>n</math>-tą liczbę pierwszą. Odkrycie G\"odla oparte jest na obserwacji, że własności formu\l\ arytmetyki mogą być wyrażane w języku samej arytmetyki jako teorioliczbowewłasności kodów. Zamiast np.&nbsp;mówić o własnościach formuły<math>\forall x_0((x_1+x_0=0)\to\bot)</math>, można mówić o własnościachjej kodu, tj. liczby <!--%--></math></center>''Kod''(\forall x_0((x_1+x_0=0)\to\bot)) =2^83^{11}5^97^911^{12}13^317^{11}19^723^129^{10}31^637^541^{10}.</math></center><!--%-->Przypomnijmy, że symbol <math>\underline n</math> oznacza term <math>\su^n('''0''')</math>. Oczywiście znaczeniem termu <math>\underline n</math> w <math>\mathfrak N</math> jest liczba&nbsp;<math>n</math>. Można teraz np.&nbsp;napisać taką formułę <math>\var\varphi(x)</math> o jednej zmiennej wolnej&nbsp;<math>x</math>, że dla dowolnego <math>n\in\NN</math> spełnianie <math>\mathfrak N\models \var\varphi(\underline n)</math> ma
+
Przypomnijmy, że symbol <math>\underline n</math> oznacza term <math>s^n(0)</math>. Oczywiście znaczeniem termu <math>\underline n</math> w <math>\mathfrak N</math> jest liczba&nbsp;<math>n</math>. Można teraz np.&nbsp;napisać taką formułę <math>\var\varphi(x)</math> o jednej zmiennej wolnej&nbsp;<math>x</math>, że dla dowolnego <math>n\in\NN</math> spełnianie <math>\mathfrak N\models \var\varphi(\underline n)</math> ma miejsce wtedy i tylko wtedy, gdy
*<math>n</math> jest numerem pewnej
 
  
 +
*<math>n</math> jest numerem pewnej formuły o co najwyżej jednej zmiennej wolnej.
  
Oczywiście wiele rozmaitych własności syntaktycznych możemy wyrazić w podobny sposób.Przydatna jest np.&nbsp;formuła <math>\sigma(x,y)</math> o takiej własności:
 
  
 +
Oczywiście wiele rozmaitych własności syntaktycznych możemy wyrazić w podobny sposób. Przydatna jest np.&nbsp;formuła <math>\sigma(x,y)</math> o takiej własności:
  
 +
<math>\mathfrak N\models \sigma(\underline n,\underline m)</math>, wtedy i tylko wtedy, gdy
  
<math>\mathfrak N\models \sigma(\underline n,\underline m)</math>, \wtw, gdy\vspace{-3mm}
 
 
*<math>m</math> jest numerem pewnej formuły <math>\alpha(x)</math> o jednej zmiennej wolnej,
 
*<math>m</math> jest numerem pewnej formuły <math>\alpha(x)</math> o jednej zmiennej wolnej,
 +
 
*<math>n</math> jest numerem zdania <math>\alpha(\underline m)</math>.
 
*<math>n</math> jest numerem zdania <math>\alpha(\underline m)</math>.
 +
 
W skrócie zapiszemy to tak:
 
W skrócie zapiszemy to tak:
  
\hfil <math>\mathfrak N\models \sigma(\underline n,\underline m)</math>, \wtw, gdy <math>n</math> jest numerem zdania <math>\alpha_m(\underline m)</math>.
+
<math>\mathfrak N\models \sigma(\underline n,\underline m)</math>, wtedy i tylko wtedy, gdy <math>n</math> jest numerem zdania <math>\alpha_m(\underline m)</math>.
  
 
Nie każda własność formuł może jednak być wyrażona w języku arytmetyki.
 
Nie każda własność formuł może jednak być wyrażona w języku arytmetyki.
  
{{twierdzenie||ttonwp|
+
{{twierdzenie|9.5 (Tarskiego o niewyrażalności prawdy)|ttonwp|
  
 +
Nie istnieje formuła wyrażająca prawdziwość formuł w standardowym modelu, tj. taka formuła <math>\pi(x)</math>, że
  
 +
<center><math>\mathfrak N\models \pi(\underline n)</math> wtedy i tylko wtedy, gdy <math>n</math> jest numerem zdania prawdziwego w&nbsp;<math>\mathfrak N</math>.</center>}}
  
Nie istnieje formuła wyrażająca prawdziwość formuł w standardowymmodelu, tj. taka formuła <math>\pi(x)</math>, że
+
{{dowod|||
  
\hfil <math>\mathfrak N\models \pi(\underline n)</math> \wtw, gdy <math>n</math> jest numerem zdania prawdziwego w&nbsp;<math>\mathfrak N</math>.}}{{dowod||
+
Dowód twierdzenia polega na wyrażeniu znanego ''paradoksu kłamcy''<ref name="trzynascie">Stwierdzenie "''To zdanie jest fałszywe''" nie może być ani prawdziwe ani fałszywe.</ref> w języku arytmetyki. Rozpatrzmy nastepującą formułę
  
Dowód twierdzenia polega na wyrażeniu znanego ''paradoksu kłamcy''\footnote{Stwierdzenie '',,\Rightarrow zdanie jest fałszywe'''' nie może być ani prawdziwe ani fałszywe.} w języku arytmetyki. Rozpatrzmy nastepującą formułę
+
<center> <math>\tau(x) \equiv  \exists y\,(\sigma(y,x)\wedge \neg \pi(y))</math>.</center>
  
\hfil <math>\tau(x) \equiv  \exists y\,(\sigma(y,x)\wedge \neg \pi(y))</math>.
+
Wówczas <math>\mathfrak N\models \tau(\underline n)</math> wtedy i tylko wtedy, gdy  
 
 
Wówczas <math>\mathfrak N\models \tau(\underline n)</math> \wtw, gdy  
 
 
*<math>n</math> jest numerem pewnej formuły <math>\alpha(x)</math> o jednej zmiennej wolnej,
 
*<math>n</math> jest numerem pewnej formuły <math>\alpha(x)</math> o jednej zmiennej wolnej,
 
*zdanie <math>\alpha(\underline n)</math> jest fałszywe w&nbsp;<math>\mathfrak N</math>.
 
*zdanie <math>\alpha(\underline n)</math> jest fałszywe w&nbsp;<math>\mathfrak N</math>.
Linia 129: Linia 147:
 
Mniej ściśle, ale prościej:
 
Mniej ściśle, ale prościej:
  
\hfil <math>\mathfrak N\models \tau(\underline n)</math> \wtw, gdy <math>\mathfrak N\models\neg\alpha_n(\underline n)</math>.
+
<center><math>\mathfrak N\models \tau(\underline n)</math> wtedy i tylko wtedy, gdy <math>\mathfrak N\models\neg\alpha_n(\underline n)</math>.</center>
  
Formuła <math>\tau(x)</math> też ma numer, powiedzmy, że <math>\tau(x) = \alpha_k(x)</math>.A zatem możemy napisać
+
Formuła <math>\tau(x)</math> też ma numer, powiedzmy, że <math>\tau(x) = \alpha_k(x)</math>. A zatem możemy napisać
  
\hfil <math>\mathfrak N\models \tau(\underline k)</math> \wtw, gdy <math>\mathfrak N\models\neg\alpha_k(\underline k)</math>.
+
<center> <math>\mathfrak N\models \tau(\underline k)</math> wtedy i tylko wtedy, gdy <math>\mathfrak N\models\neg\alpha_k(\underline k)</math>.</center>
  
 
Możemy to napisać z czystym sumieniem, bo warunek  
 
Możemy to napisać z czystym sumieniem, bo warunek  
*<math>k</math> jest numerem pewnej formuły <math>\alpha(x)</math> o jednej zmiennej wolnej,
 
 
  
jest oczywiście spełniony. Ale przecież <math>\alpha_k(\underline k)</math> to właśnieformuła <math>\tau(\underline k)</math>. A zatem:
+
*<math>k</math> jest numerem pewnej formuły <math>\alpha(x)</math> o jednej zmiennej wolnej
  
\hfil <math>\mathfrak N\models \tau(\underline k)</math> \wtw, gdy <math>\mathfrak N\models\neg \tau(\underline k)</math>.
+
jest oczywiście spełniony. Ale przecież <math>\alpha_k(\underline k)</math> to właśnie formuła <math>\tau(\underline k)</math>. A zatem:
  
No jasne: zdanie <math>\tau(\underline k)</math> stwierdza '',,Ja jestem fałszywe!''''Ze znanym skutkiem \dots}}
+
<center> <math>\mathfrak N\models \tau(\underline k)</math> wtedy i tylko wtedy, gdy <math>\mathfrak N\models\neg \tau(\underline k)</math>.</center>
  
'''Uwaga:''' Twierdzenie Tarskiego podpowiada rozstrzygnięcie paradoksu kłamcy: Problem leży w niewyrażalności pojęcia ,,zdania prawdziwego'',także w języku polskim. A skoro pytamy o&nbsp;własność, której nieumiemy zdefiniować, to nie dziwmy się, że nie ma odpowiedzi.  
+
No jasne: zdanie <math>\tau(\underline k)</math> stwierdza "''Ja jestem fałszywe!''" Ze znanym skutkiem ...}}
  
 +
'''Uwaga:''' Twierdzenie Tarskiego podpowiada rozstrzygnięcie paradoksu kłamcy: Problem leży w niewyrażalności pojęcia "zdania prawdziwego", także w języku polskim. A skoro pytamy o&nbsp;własność, której nieumiemy zdefiniować, to nie dziwmy się, że nie ma odpowiedzi.
  
  
Twierdzenie G\"odla o niezupełności arytmetyki otrzymamy po nieznacznej modyfikacji powyższego rozumowania. Zamiast niemożliwego do zdefiniowaniapojęcia prawdy,użyjemy wyrażalnej własności ,,mieć dowód w arytmetycePeano''. Otrzymamy w ten sposób zdanie&nbsp;<math>Z</math>, które mówi: ,,''Ja nie mam dowodu!''''.
+
Twierdzenie Gödla o niezupełności arytmetyki otrzymamy po nieznacznej modyfikacji powyższego rozumowania. Zamiast niemożliwego do zdefiniowania pojęcia prawdy, użyjemy wyrażalnej własności "mieć dowód w arytmetyce Peano". Otrzymamy w ten sposób zdanie&nbsp;<math>Z</math>, które mówi: ""''Ja nie mam dowodu!''".
  
'''Inny dowód Twierdzenia&nbsp;[[#tgonzap]]: '''Postępujemy jak w poprzednim dowodzie,używając formuły<math>\pi'(x)</math> o własności
+
'''Inny dowód [[#tgonzap|Twierdzenia 9.4]]: Postępujemy jak w poprzednim dowodzie,używając formuły<math>\pi'(x)</math> o własności
  
<math>\mathfrak N\models \pi'(\underline n)</math> \wtw, gdy <math>n</math> jest numerem %pewnego zdania, które ma dowód w&nbsp;PA.
+
<center><math>\mathfrak N\models \pi'(\underline n)</math> wtedy i tylko wtedy, gdy <math>n</math> jest numerem pewnego zdania, które ma dowód w&nbsp;PA.</center>
  
Otrzymamy w końcu taką konkluzję:<math>\mathfrak N\models \tau(\underline k)</math> \wtw, gdy <math>{\rm PA}\not\vdash_H \tau(\underline k)</math>.
+
Otrzymamy w końcu taką konkluzję: <math>\mathfrak N\models \tau(\underline k)</math> wtedy i tylko wtedy, gdy <math>{\rm PA}\not\vdash_H \tau(\underline k)</math>.
  
Przyjmując <math>Z = \tau(\underline k)</math>, wnioskujemy, że ani <math>Z</math> ani <math>\neg Z</math> niemoże mieć dowodu w&nbsp;PA. Założenie <math>PA\vdash_H Z</math> prowadzi do sprzeczności, bo jeśli <math>PA\vdash_H Z</math> to <math>\mathfrak N\models Z</math>. Ale założenie <math>PA\vdash_H\neg Z</math> też prowadzi do sprzeczności, bo mielibyśmy z jednej strony <math>\mathfrak N\models\neg Z</math>,a z drugiej <math>\mathfrak N\models Z</math>. Uwaga: nietrudno zauważyć, że <math>\mathfrak N\models Z</math>.\hfil\qed
+
Przyjmując <math>Z = \tau(\underline k)</math>, wnioskujemy, że ani <math>Z</math> ani <math>\neg Z</math> nie może mieć dowodu w&nbsp;PA. Założenie <math>PA\vdash_H Z</math> prowadzi do sprzeczności, bo jeśli <math>PA\vdash_H Z</math> to <math>\mathfrak N\models Z</math>. Ale założenie <math>PA\vdash_H\neg Z</math> też prowadzi do sprzeczności, bo mielibyśmy z jednej strony <math>\mathfrak N\models\neg Z</math>, a z drugiej <math>\mathfrak N\models Z</math>. Uwaga: nietrudno zauważyć, że <math>\mathfrak N\models Z</math>.
  
Rozumowanie G\"odla prowadzi do jeszcze jednego ważnego wniosku, nazywanego''drugim twierdzeniem o niezupełności''. Niech <math>m</math> będzie numerem zdania ,,<math>0=\su(0)</math>'' i niech '''Con''' oznacza zdanie <math>\neg \pi'(\underline m)</math>. Zdanie to wyraża niesprzeczność arytmetyki Peano. Rozumowanie podobne doużytego w dowodzie Twierdzenia&nbsp;[[#tgonzap]] można\dots&nbsp;sformalizować w języku arytmetyki. Otrzymamy konkluzję:
 
  
\hfil <math>{\rm PA}\vdash_H '''Con''' \to Z</math>,
 
  
gdzie <math>Z</math> jest zdaniem z Twierdzenia&nbsp;[[#tgonzap]]. W konsekwencjiotrzymujemy:
+
Rozumowanie Gödla prowadzi do jeszcze jednego ważnego wniosku, nazywanego ''drugim twierdzeniem o niezupełności''. Niech <math>m</math> będzie numerem zdania "<math>0=s(0)</math>" i niech '''Con''' oznacza zdanie <math>\neg \pi'(\underline m)</math>. Zdanie to wyraża niesprzeczność arytmetyki Peano. Rozumowanie podobne doużytego w dowodzie [[#tgonzap|Twierdzenia 9.4]] można ...&nbsp;sformalizować w języku arytmetyki. Otrzymamy konkluzję:
  
{{wniosek||panoncon|
+
<center> <math>{\rm PA}\vdash_H Con \to Z</math>,</center>
  
 +
gdzie <math>Z</math> jest zdaniem z [[#tgonzap|Twierdzenia 9.4]]. W konsekwencji otrzymujemy:
  
 +
{{wniosek|9.6|panoncon|
 +
<math>{\rm PA}\not\vdash_H Con</math>.}}
  
<math>{\rm PA}\not\vdash_H '''Con'''</math>.}}\vspace{-2mm}Niesprzeczności arytmetyki Peano nie możnaudowodnić na grunciesamej arytmetyki Peano (chyba, że PA jest sprzeczna). Ta sama konkluzja dotyczy każdej dostatecznie silnej teorii.
+
Niesprzeczności arytmetyki Peano nie można udowodnić na gruncie samej arytmetyki Peano (chyba, że PA jest sprzeczna). Ta sama konkluzja dotyczy każdej dostatecznie silnej teorii.
  
Na zakończenie powiedzmy jeszcze, że teoria PA jest nierozstrzygalna.Dowód tego faktu wymaga pewnegoudoskonalenia Twierdzenia&nbsp;[[#expr]].Zamiast równoważności  
+
Na zakończenie powiedzmy jeszcze, że teoria PA jest nierozstrzygalna. Dowód tego faktu wymaga pewnego udoskonalenia [[#expr|Twierdzenia 9.2]]. Zamiast równoważności  
  
\hfil <math>\sat\mathfrak N\varrho\var\varphi</math> \quad \wtw, gdy\quad <math>f(n_1,\ldots,n_k)=m</math>,
+
<center><math>(\mathfrak N\varrho)\models\var\varphi</math> wtedy i tylko wtedy, gdy  <math>f(n_1,\ldots,n_k)=m</math>,</center>
  
 
można mianowicie pokazać równoważność postaci
 
można mianowicie pokazać równoważność postaci
  
\hfil </math>{\rm PA}\vdash_H\var\varphi(\underline n_1,\ldots,\underline n_k,\underline m)</math> \quad \wtw, gdy\quad  <math>f(n_1,\ldots,n_k)=m</math>.  
+
<center> <math>{\rm PA}\vdash_H\var\varphi(\underline n_1,\ldots,\underline n_k,\underline m)</math> wtedy i tylko wtedy, gdy <math>f(n_1,\ldots,n_k)=m</math>. </center>
  
Nierozstrzygalność PA możnaudowodnić metodą podobną doużytej w dowodzie Wniosku&nbsp;[[#przescieradlo]].<!--%-->\subsection*{Ćwiczenia}\begin{small}
+
Nierozstrzygalność PA można udowodnić metodą podobną do użytej w dowodzie [[#przescieradlo|Wniosku 9.3]].
#Udowodnić, że istnieje niestandardowy, przeliczalny model <math>Th(\mathfrak N)</math>, a w nim liczba, mająca nieskończenie wiele dzielników pierwszych.
 
#Pokazać, że następujące zdania są twierdzeniami arytmetyki Peano:
 
##<math>\underline 2\cdot \underline 2 = \underline 4</math>;
 
##<math>\forall{x}\ciut(\neg({x}=0)\to\exists {y}\ciut({x}=\su(y)))</math>;
 
##<math>\forall{x}\forall{y}\forall{z}\ciut (({x}+{y})+{z}={x}+({y}+{z}))</math>;
 
##<math>\forall{x}\forall{y}\ciut ({x}+{y}={y}+{x})</math>;
 
\item Jaka jest różnica pomiędzy następującymi zdaniami?
 
*''Dwa razy dwa jest cztery.''
 
''Wskazówka:'' Pierwsze zdanie mówi o pewnej własności liczb. Żeby się z nim zgodzić, wystarczy wiedzieć ile jest dwa razy dwa. Co trzeba wiedzieć, aby zrozumieć drugie zdania?
 

Aktualna wersja na dzień 09:16, 30 paź 2006

Słowo arytmetyka używane jest w odniesieniu do różnych teorii dotyczących liczb naturalnych. Nasza sygnatura dla arytmetyki pierwszego rzędu składa się z dwuargumentowych symboli funkcyjnych i , oznaczających dodawanie i mnożenie, symbolu następnika s oraz stałej 0.

Skoro przedmiotem arytmetyki są liczby naturalne, strukturę Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle \mathfrak N = <\mathbb N, +,\cdot, 0, \su>} ze "zwykłymi" operacjami arytmetycznymi nazwiemy standardowym modelem arytmetyki. Zbiór złożony ze wszystkich zdań prawdziwych w modelu nazywiemy zaś arytmetyką zupełną. Niestety,arytmetyka zupełna nie wyznacza modelu standardowego jednoznacznie.

Fakt 9.1

Dla dowolnej mocy Parser nie mógł rozpoznać (nieznana funkcja „\frak”): {\displaystyle {\frak m}\geq\aleph_0} istnieje niestandardowy model arytmetyki mocy Parser nie mógł rozpoznać (nieznana funkcja „\frak”): {\displaystyle {\frak m}} , tj. struktura mocy Parser nie mógł rozpoznać (nieznana funkcja „\frak”): {\displaystyle {\frak m}}

,
która jest elementarnie równoważna , ale nieizomorficzna z .


Dowód

Niech składa się ze wszystkich formuł postaci . Nietrudno pokazać, że każdy skończony podzbiór zbioru jest spełnialny w modelu  przez dostatecznie dużą wartość . Na mocy twierdzenia o zwartości (Twierdzenie 8.1), całość jest spełnialna w pewnym modelu  przez pewne wartościowanie . Wtedy spełnia te same zdania co , ale element nie ma odpowiednika w modelu , bo każdy element można otrzymać z zera za pomocą nastepnika. Z Twierdzenia 8.2 wynika, że model  może być żądanej mocy.

End of proof.gif

Powyższy fakt to kolejny przykład wskazujący na ograniczenia siły wyrazu logiki pierwszego rzędu. Pora więc na pewne obserwacje o charakterze pozytywnym. Język arytmetyki jest tak elastyczny, że można w nim zdefiniować każdą funkcję obliczalną.

Twierdzenie 9.2 (Gödel)

Dla dowolnej częściowej funkcji obliczalnej istnieje taka formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV(\var\varphi)\subseteq\{x_1,\ldots,x_k,y\}} oraz dla zachodzi równoważność

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak N,\varrho)\models\var\varphi} wtedy i tylko wtedy, gdy .

Dowód Twierdzenia 9.2 opuszczamy. Istotnym problemem technicznym w tym dowodzie jest konieczność kodowania ciągów liczb o nieznanej z góry długości. Używa się w tym celu tzw. chińskiego twierdzenia o resztach.


Wniosek 9.3

Teoria jest nierozstrzygalna. Co więcej, ani zbiór , ani jego dopełnienie nie są nawet rekurencyjnie przeliczalne.

Dowód

Z Twierdzenia 9.2 wynika w szczególności, że dla dowolnego zbioru rekurencyjnie przeliczalnego Parser nie mógł rozpoznać (nieznana funkcja „\NN”): {\displaystyle A\subseteq\NN} istnieje formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(x)} , o jednej zmiennej wolnej , dla której

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak N,x:n)\models\var\varphi} wtedy i tylko wtedy, gdy .

Korzystając z Lematu 2.10, możemy napisać to tak:

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(\underline n)\in Th(\mathfrak N)} wtedy i tylko wtedy, gdy ,

gdzie symbol oznacza term . A więc rozstrzygalność implikowałaby rozstrzygalność problemu stopu.

Aby udowodnić drugą część twierdzenia, przypomnijmy, że problem decyzyjny

Czy dana maszyna Turinga zatrzymuje się dla każdego słowa wejściowego?

nie jest częściowo rozstrzygalny, i że to samo dotyczy jego dopełnienia. Jeśli zakodujemy nasz problem w postaci zbioru , to zbiór ten będzie można zdefiniować formułą arytmetyki z dwoma kwantyfikatorami, wyrażającą własność

Dla każdego (kodu) słowa istnieje kod obliczenia akceptującego to słowo.

Zbiór jest więc też definiowalny formułą arytmetyki i byłby rekurencyjnie przeliczalny, gdyby taka była teoria .

End of proof.gif

Twierdzenie Gödla o niezupełności

Skoro nie można zdefiniować jednoznacznie modelu standardowego(Fakt 9.1), może można chociaż, za pomocą odpowiednich aksjomatów, scharakteryzować zdania które są w nim prawdziwe? Przez PA (od "Peano Arithmetics") oznaczymy teorię o aksjomatach:

  • ;
  • ;
  • ;
  • ;
  • ;
  • Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x (\var\varphi(x)\to\var\varphi(s(x)))\to(\var\varphi(0)\to\forall x\,\var\varphi(x))} ,

gdzie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(x)} może być dowolną formułą. Pierwsze dwa aksjomaty mówią, że operacja następnika jest różnowartościowa, a zero nie jest następnikiem żadnej liczby (to gwarantuje nieskończoność każdego modelu). Kolejne dwa aksjomaty stanowią indukcyjną definicję dodawania, a następne dwa --- indukcyjną definicję mnożenia. Na końcu zamiast pojedynczego aksjomatu, mamy schemat aksjomatu, nazywany schematem indukcji. Zatem zbiór aksjomatów Peano jest w istocie nieskończony. Ale zbiór ten jest rekurencyjny: można efektywnie ustalić co jest aksjomatem, a co nie jest.

Oczywiście standardowy model arytmetyki jest modelem arytmetyki Peano:

Inaczej mówiąc, wszystkie konsekwencje aksjomatów Peano (twierdzenia teorii PA) są prawdziwe w standardowym modelu. A na odwrót? Kiedyś przypuszczano, że PA jest teorią zupełną (por. Definicja 4.14), tj. że każde zdanie prawdziwe w jest twierdzeniem arytmetyki Peano.

Przypuszczenie to okazało się fałszywe dzięki odkryciu dokonanemu przez Gödla, a mianowicie dzięki metodzie arytmetyzacji (numeracji Göodla), która pozwoliła na wyrażanie w języku arytmetyki faktów odnoszących się do samej arytmetyki, w szczególności istnienia lub nieistnienia dowodu dla danej formuły.

Twierdzenie 9.4 (Gödla o niezupełności

Istnieje takie zdanie w języku arytmetyki, że .

Dowód

Skoro zbiór aksjomatów PA jest rekurencyjny, więc zbiór wszystkich twierdzeń teorii PA (formuł, które można wyprowadzić z tych aksjomatów) jest rekurencyjnie przeliczalny. Aby bowiem stwierdzić, że dana formuła jest twierdzeniem PA, wystarczy systematycznie generować wszystkie możliwe dowody, aż wreszcie otrzymamy ten właściwy.

Gdyby PA była teorią zupełną, to dla dowolnego zdania Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , prędzej czy później znaleźlibyśmy albo dowód formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} albo formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi} . A więc w takim przypadku PA byłaby po prostu rozstrzygalna.

Ale z drugiej strony, teoria zupełna jest identyczna z teorią każdego swojego modelu, więc PA byłaby identyczna z . Wówczas jednak teoria musiałaby być rozstrzygalna, co przeczy Wnioskowi 9.3.

End of proof.gif

Istota twierdzenia Gödla polega nie na tym, że akurat PA jest niezupełna. Jeśli zbiór aksjomatów PA rozszerzymy do innego (rekurencyjnie przeliczalnego) zbioru aksjomatów prawdziwych w , to nadal będzie istniało zdanie niezależne od tych aksjomatów. Dowód pozostanie prawie bez zmian. A więc nie tylko PA, ale w ogóle każda efektywnie zadana teoria musi być niezupełna, jeśli tylko jest dostatecznie silna na to, aby dało sie w niej zinterpretować pojęcia arytmetyczne.

Przytoczony powyżej "współczesny" dowód twierdzenia Gödla wykorzystuje numerację gödlowską pośrednio, poprzez odwołanie się do pojęcia rozstrzygalnego problemu decyzyjnego. (Mówiąc o algorytmach generujących dowody, w istocie mamy na myśli pewne obliczenia na kodach takich dowodów, itd.). Oryginalny dowód Göodla posługiwał się numeracją bezpośrednio i przebiegał mniej więcej tak jak niżej. Na początek numerujemy wszystkie symbole języka arytmetyki:

Symbol: Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall\} ( )
Numer: 1 2 3 4 5 6 7 8 9 10 11 12

Każdemu ciągowi znaków, w tym każdej formule, dowodowi itp., można teraz przypisać kod liczbowy. Jeśli przez oznaczymy numer znaku , to kodem napisu "" jest liczba

gdzie oznacza -tą liczbę pierwszą. Odkrycie Gödla oparte jest na obserwacji, że własności formuł arytmetyki mogą być wyrażane w języku samej arytmetyki jako teorioliczbowe własności kodów. Zamiast np. mówić o własnościach formuły, można mówić o własnościach jej kodu, tj. liczby


Przypomnijmy, że symbol oznacza term . Oczywiście znaczeniem termu w jest liczba . Można teraz np. napisać taką formułę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(x)} o jednej zmiennej wolnej , że dla dowolnego Parser nie mógł rozpoznać (nieznana funkcja „\NN”): {\displaystyle n\in\NN} spełnianie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak N\models \var\varphi(\underline n)} ma miejsce wtedy i tylko wtedy, gdy

  • jest numerem pewnej formuły o co najwyżej jednej zmiennej wolnej.


Oczywiście wiele rozmaitych własności syntaktycznych możemy wyrazić w podobny sposób. Przydatna jest np. formuła o takiej własności:

, wtedy i tylko wtedy, gdy

  • jest numerem pewnej formuły o jednej zmiennej wolnej,
  • jest numerem zdania .

W skrócie zapiszemy to tak:

, wtedy i tylko wtedy, gdy jest numerem zdania .

Nie każda własność formuł może jednak być wyrażona w języku arytmetyki.

Twierdzenie 9.5 (Tarskiego o niewyrażalności prawdy)

Nie istnieje formuła wyrażająca prawdziwość formuł w standardowym modelu, tj. taka formuła , że

wtedy i tylko wtedy, gdy jest numerem zdania prawdziwego w .

Dowód

{{{3}}} End of proof.gif

Uwaga: Twierdzenie Tarskiego podpowiada rozstrzygnięcie paradoksu kłamcy: Problem leży w niewyrażalności pojęcia "zdania prawdziwego", także w języku polskim. A skoro pytamy o własność, której nieumiemy zdefiniować, to nie dziwmy się, że nie ma odpowiedzi.


Twierdzenie Gödla o niezupełności arytmetyki otrzymamy po nieznacznej modyfikacji powyższego rozumowania. Zamiast niemożliwego do zdefiniowania pojęcia prawdy, użyjemy wyrażalnej własności "mieć dowód w arytmetyce Peano". Otrzymamy w ten sposób zdanie , które mówi: ""Ja nie mam dowodu!".

Inny dowód Twierdzenia 9.4: Postępujemy jak w poprzednim dowodzie,używając formuły o własności

wtedy i tylko wtedy, gdy jest numerem pewnego zdania, które ma dowód w PA.

Otrzymamy w końcu taką konkluzję: wtedy i tylko wtedy, gdy .

Przyjmując , wnioskujemy, że ani ani nie może mieć dowodu w PA. Założenie prowadzi do sprzeczności, bo jeśli to . Ale założenie też prowadzi do sprzeczności, bo mielibyśmy z jednej strony , a z drugiej . Uwaga: nietrudno zauważyć, że .


Rozumowanie Gödla prowadzi do jeszcze jednego ważnego wniosku, nazywanego drugim twierdzeniem o niezupełności. Niech będzie numerem zdania "" i niech Con oznacza zdanie . Zdanie to wyraża niesprzeczność arytmetyki Peano. Rozumowanie podobne doużytego w dowodzie Twierdzenia 9.4 można ... sformalizować w języku arytmetyki. Otrzymamy konkluzję:

,

gdzie jest zdaniem z Twierdzenia 9.4. W konsekwencji otrzymujemy:

Wniosek 9.6

.

Niesprzeczności arytmetyki Peano nie można udowodnić na gruncie samej arytmetyki Peano (chyba, że PA jest sprzeczna). Ta sama konkluzja dotyczy każdej dostatecznie silnej teorii.

Na zakończenie powiedzmy jeszcze, że teoria PA jest nierozstrzygalna. Dowód tego faktu wymaga pewnego udoskonalenia Twierdzenia 9.2. Zamiast równoważności

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak N\varrho)\models\var\varphi} wtedy i tylko wtedy, gdy ,

można mianowicie pokazać równoważność postaci

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle {\rm PA}\vdash_H\var\varphi(\underline n_1,\ldots,\underline n_k,\underline m)} wtedy i tylko wtedy, gdy .

Nierozstrzygalność PA można udowodnić metodą podobną do użytej w dowodzie Wniosku 9.3.