Logika dla informatyków/Arytmentyka pierwszego rzędu

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 $\cdot \,$, 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 $Th({\mathfrak {N}})$ złożony ze wszystkich zdań prawdziwych w modelu ${\mathfrak {N}}$ 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}}

${\mathfrak {M}}=<\mathbb {M} ,\oplus ,\otimes ,0,S>$, która jest elementarnie równoważna ${\mathfrak {N}}$, ale nieizomorficzna z ${\mathfrak {N}}$.

Dowód

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

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 $f:\mathbb {N} ^{k}\rightarrow \mathbb {N}$ 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 $\varrho (x_{1})=n_{1},\ldots ,\varrho (x_{k})=n_{k},\varrho (y)=m$ zachodzi równoważność

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

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 $Th({\mathfrak {N}})$ jest nierozstrzygalna. Co więcej, ani zbiór $Th({\mathfrak {N}})$, 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 $x$, dla której

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

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 $n\in A$,

gdzie symbol ${\underline {n}}$ oznacza term $s^{n}(0)$. A więc rozstrzygalność $Th({\mathfrak {N}})$ 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 $A\subseteq \mathbb {N}$, 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 $w$ istnieje kod obliczenia akceptującego to słowo.

Zbiór $A$ jest więc też definiowalny formułą arytmetyki i byłby rekurencyjnie przeliczalny, gdyby taka była teoria $Th({\mathfrak {N}})$.

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:

• $\forall x\forall y\,(s(x)=s(y)\to x=y)$;
• $\forall x\neg (s(x)=0)$
• $\forall x\ (x+0=x)$;
• $\forall x\forall y\ (x+s(y)=s(x+y))$;
• $\forall x(x\cdot 0=0)$;
• $\forall x\forall y\ (x\cdot s(y)=(x\cdot y)+x)$;
• 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:

${\mathfrak {N}}\models {\rm {PA}}.$

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 ${\mathfrak {N}}$ 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 $Z$ w języku arytmetyki, że ${\rm {PA}}\not \vdash _{H}Z$ i ${\rm {PA}}\not \vdash _{H}\neg Z$.

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 $Th({\mathfrak {N}})$. Wówczas jednak teoria $Th({\mathfrak {N}})$ musiałaby być rozstrzygalna, co przeczy 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 ${\mathfrak {N}}$, 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:	$0$	$s$	$+$	$\cdot$	$\bot$	$\to$	$=$	Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall\}	(	)	$x_{0}$	$x_{1}$	$\dots$
Numer:	1	2	3	4	5	6	7	8	9	10	11	12	$\dots$

Każdemu ciągowi znaków, w tym każdej formule, dowodowi itp., można teraz przypisać kod liczbowy. Jeśli przez $\#a$ oznaczymy numer znaku $a$, to kodem napisu "$a_{1}a_{2}\ldots a_{n}$" jest liczba

$Kod(a_{1}a_{2}\ldots a_{n})=2^{\#a_{1}}3^{\#a_{2}}5^{\#a_{3}}7^{\#a_{4}\cdots }p_{n}^{\#a_{n}},$

gdzie $p_{n}$ oznacza $n$-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$\forall x_{0}((x_{1}+x_{0}=0)\to \bot )$, można mówić o własnościach jej kodu, tj. liczby

$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}.$

Przypomnijmy, że symbol ${\underline {n}}$ oznacza term $s^{n}(0)$. Oczywiście znaczeniem termu ${\underline {n}}$ w ${\mathfrak {N}}$ jest liczba $n$. Można teraz np. napisać taką formułę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(x)} o jednej zmiennej wolnej $x$, ż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

• $n$ 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 $\sigma (x,y)$ o takiej własności:

${\mathfrak {N}}\models \sigma ({\underline {n}},{\underline {m}})$, wtedy i tylko wtedy, gdy

• $m$ jest numerem pewnej formuły $\alpha (x)$ o jednej zmiennej wolnej,

• $n$ jest numerem zdania $\alpha ({\underline {m}})$.

W skrócie zapiszemy to tak:

${\mathfrak {N}}\models \sigma ({\underline {n}},{\underline {m}})$, wtedy i tylko wtedy, gdy $n$ jest numerem zdania $\alpha _{m}({\underline {m}})$.

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 $\pi (x)$, że

${\mathfrak {N}}\models \pi ({\underline {n}})$ wtedy i tylko wtedy, gdy $n$ jest numerem zdania prawdziwego w ${\mathfrak {N}}$.

Dowód

{{{3}}}

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 $Z$, 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$\pi '(x)$ o własności

${\mathfrak {N}}\models \pi '({\underline {n}})$ wtedy i tylko wtedy, gdy $n$ jest numerem pewnego zdania, które ma dowód w PA.

Otrzymamy w końcu taką konkluzję: ${\mathfrak {N}}\models \tau ({\underline {k}})$ wtedy i tylko wtedy, gdy ${\rm {PA}}\not \vdash _{H}\tau ({\underline {k}})$.

Przyjmując $Z=\tau ({\underline {k}})$, wnioskujemy, że ani $Z$ ani $\neg Z$ nie może mieć dowodu w PA. Założenie $PA\vdash _{H}Z$ prowadzi do sprzeczności, bo jeśli $PA\vdash _{H}Z$ to ${\mathfrak {N}}\models Z$. Ale założenie $PA\vdash _{H}\neg Z$ też prowadzi do sprzeczności, bo mielibyśmy z jednej strony ${\mathfrak {N}}\models \neg Z$, a z drugiej ${\mathfrak {N}}\models Z$. Uwaga: nietrudno zauważyć, że ${\mathfrak {N}}\models Z$.

Rozumowanie Gödla prowadzi do jeszcze jednego ważnego wniosku, nazywanego drugim twierdzeniem o niezupełności. Niech $m$ będzie numerem zdania "$0=s(0)$" i niech Con oznacza zdanie $\neg \pi '({\underline {m}})$. 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ę:

${\rm {PA}}\vdash _{H}Con\to Z$,

gdzie $Z$ jest zdaniem z Twierdzenia 9.4. W konsekwencji otrzymujemy:

Wniosek 9.6

${\rm {PA}}\not \vdash _{H}Con$.

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 $f(n_{1},\ldots ,n_{k})=m$,

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 $f(n_{1},\ldots ,n_{k})=m$.

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