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, więc 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}}$, aleelement $\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

Dla dowolnej częściowej funkcji obliczalnej Parser nie mógł rozpoznać (nieznana funkcja „\shortrightarrows”): {\displaystyle f:\mathbb N^k\shortrightarrows\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, gdyd $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

Teoria $'''Th'''({\mathfrak {N}})$ jest nierozstrzygalna. Co więcej, ani zbiór $'''Th'''({\mathfrak {N}})$, ani jego dopełnienie nie są nawet rekurencyjnieprzeliczalne.

Dowód

{{{3}}}

Skoro nie można zdefiniować jednoznacznie modelu standardowego(Fakt #ranny), 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 „\su”): {\displaystyle \forall x\forall y\,(\su(x)=\su(y)\to x=y)} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle \forall x\neg (\su(x)=0)}
• $\forall x\,(x+0=x)$;
• Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle \forall x\forall y\,(x+\su(y) = \su(x+y))} ;
• $\forall x\,(x\cdot 0=0)$;
• Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle \forall x\forall y\,(x\cdot\su(y) = (x\cdot y)+x)} ;
• </math>\forall x\,(\var\varphi(x)\to\var\varphi(\su(x)))\to(\var\varphi(0)\to\forall x\,\var\varphi(x)</math>),

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 gwarantujenieskoń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żnaefektywnieustalić 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 (twierdzeniateorii PA) są prawdziwe w standardowym modelu. A na odwrót? Kiedyś przypuszczano, że PA jest teorią zupełną (por. Definicja #slmFOjof), tj. że każde zdanie prawdziwe w ${\mathfrak {N}}$ 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.

Twierdzenie

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

{{{3}}}

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 ${\mathfrak {N}}$ 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.

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:

\begin{tabbing}Symbol: \=\quad $0$\quad \=\quad Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle \su} \quad \=\quad $+$\quad \=\quad $\cdot$\quad\=$\quad \bot$\quad\=$\quad \to \quad$\=$\quad =\quad$\=$\quad \forall \quad$\=\quad (\quad \=\quad\ )\quad \=$\quad x_{0}\quad$\=$\quad x_{1}\quad$\=\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 $\#a$ oznaczymy numer znaku $a$, to kodem napisu ,,$a_{1}a_{2}\ldots a_{n}$ jest liczba </math>Kod\/}(a_1a_2\ldots a_n) = 2^{\#a_1}3^{\#a_2}5^{\#a_3}7^{\#a_4\cdotsp_n^{\#a_n},</math>gdzie $p_{n}$ oznacza $n$-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. 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ściachjej kodu, tj. liczby </math>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>Przypomnijmy, że symbol ${\underline {n}}$ oznacza term Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle \su^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

• $n$ jest numerem pewnej

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}})$, \wtw, gdy\vspace{-3mm}

• $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:

\hfil ${\mathfrak {N}}\models \sigma ({\underline {n}},{\underline {m}})$, \wtw, 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

Nie istnieje formuła wyrażająca prawdziwość formuł w standardowymmodelu, tj. taka formuła $\pi (x)$, że

\hfil ${\mathfrak {N}}\models \pi ({\underline {n}})$ \wtw, 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\"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 $Z$, które mówi: ,,Ja nie mam dowodu!'.

Inny dowód Twierdzenia #tgonzap: Postępujemy jak w poprzednim dowodzie,używając formuły$\pi '(x)$ o własności

${\mathfrak {N}}\models \pi '({\underline {n}})$ \wtw, 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}})$ \wtw, gdy ${\rm {PA}}\not \vdash _{H}\tau ({\underline {k}})$.

Przyjmując $Z=\tau ({\underline {k}})$, wnioskujemy, że ani $Z$ ani $\neg Z$ niemoż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$.\hfil\qed

Rozumowanie G\"odla prowadzi do jeszcze jednego ważnego wniosku, nazywanegodrugim twierdzeniem o niezupełności. Niech $m$ będzie numerem zdania ,,Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle 0=\su(0)} i niech Con oznacza zdanie $\neg \pi '({\underline {m}})$. Zdanie to wyraża niesprzeczność arytmetyki Peano. Rozumowanie podobne doużytego w dowodzie Twierdzenia #tgonzap można\dots sformalizować w języku arytmetyki. Otrzymamy konkluzję:

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

gdzie $Z$ jest zdaniem z Twierdzenia #tgonzap. W konsekwencjiotrzymujemy:

Wniosek

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

\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.

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

\hfil Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\mathfrak N\varrho\var\varphi} \quad \wtw, gdy\quad $f(n_{1},\ldots ,n_{k})=m$,

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

Nierozstrzygalność PA możnaudowodnić metodą podobną doużytej w dowodzie Wniosku #przescieradlo.\subsection*{Ćwiczenia}\begin{small}

1. Udowodnić, że istnieje niestandardowy, przeliczalny model $Th({\mathfrak {N}})$, a w nim liczba, mająca nieskończenie wiele dzielników pierwszych.
2. Pokazać, że następujące zdania są twierdzeniami arytmetyki Peano:
   1. ${\underline {2}}\cdot {\underline {2}}={\underline {4}}$;
   2. Parser nie mógł rozpoznać (nieznana funkcja „\ciut”): {\displaystyle \forall{x}\ciut(\neg({x}=0)\to\exists {y}\ciut({x}=\su(y)))} ;
   3. Parser nie mógł rozpoznać (nieznana funkcja „\ciut”): {\displaystyle \forall{x}\forall{y}\forall{z}\ciut (({x}+{y})+{z}={x}+({y}+{z}))} ;
   4. Parser nie mógł rozpoznać (nieznana funkcja „\ciut”): {\displaystyle \forall{x}\forall{y}\ciut ({x}+{y}={y}+{x})} ;

\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?