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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Linia 14: Linia 14:
 
{{dowod|||
 
{{dowod|||
  
Niech <math>\Delta</math> składa się ze wszystkich formuł postaci <math>x\not=s(s(\ldotss(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 dostateczniedużą 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 dostateczniedużą 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.
 
}}
 
}}
  

Wersja z 12:12, 22 wrz 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, 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 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 dostateczniedużą 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 , aleelement 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 takelastyczny, że można w nim zdefiniować każdą funkcję obliczalną.

Twierdzenie

{{{3}}}

Dowód Twierdzenia #expr 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 jest nierozstrzygalna. Co więcej, ani zbiór , ani jego dopełnienie nie są nawet rekurencyjnieprzeliczalne.

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

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)}
  • ;
  • Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle \forall x\forall y\,(x+\su(y) = \su(x+y))} ;
  • ;
  • 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:

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 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 w języku arytmetyki, że .

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

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 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 \quad \=\quad Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle \su} \quad \=\quad \quad \=\quad \quad\=\quad\=\=\=\=\quad (\quad \=\quad\ )\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 oznaczymy numer znaku , to kodem napisu ,, 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 oznacza -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, 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 oznacza term Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle \su^n('''0''')} . 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

  • jest numerem pewnej


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:


, \wtw, gdy\vspace{-3mm}

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

W skrócie zapiszemy to tak:

\hfil , \wtw, gdy jest numerem zdania .

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 , że

\hfil \wtw, gdy jest numerem zdania prawdziwego w .

{{{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\"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 , które mówi: ,,Ja nie mam dowodu!'.

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

\wtw, gdy jest numerem %pewnego zdania, które ma dowód w PA.

Otrzymamy w końcu taką konkluzję: \wtw, gdy .

Przyjmując , wnioskujemy, że ani ani niemoż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 .\hfil\qed

Rozumowanie G\"odla prowadzi do jeszcze jednego ważnego wniosku, nazywanegodrugim twierdzeniem o niezupełności. Niech będzie numerem zdania ,,Parser nie mógł rozpoznać (nieznana funkcja „\su”): {\displaystyle 0=\su(0)} i niech Con oznacza zdanie . 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 ,

gdzie jest zdaniem z Twierdzenia #tgonzap. W konsekwencjiotrzymujemy:

Wniosek


.

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

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 .

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

  1. Udowodnić, że istnieje niestandardowy, przeliczalny model , a w nim liczba, mająca nieskończenie wiele dzielników pierwszych.
  2. Pokazać, że następujące zdania są twierdzeniami arytmetyki Peano:
    1. ;
    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?