Twierdzenia Gödla

$% \usepackage{amsmath} % \usepackage{amsfonts} % \usepackage{amssymb} % create the definition symbol \def\bydef{\stackrel{\text{def}}{=}} \newcommand{\qed}{\mbox{ } \Box} \newcommand{\set}[1]{\{#1\}} \newcommand{\eps}{\varepsilon} \newcommand{\NN}{\mathbb N} \newcommand{\Nat}{\mathbb N} \newcommand{\RR}{\mathbb R} \newcommand{\Aa}{\mathcal A} \newcommand{\Bb}{\mathcal B} \newcommand{\Cc}{\mathcal C} \newcommand{\Dd}{\mathcal D} \newcommand{\Ll}{\mathcal L} \newcommand{\str}[1]{\mathbb {#1}} \renewcommand{\implies}{\rightarrow} \newcommand{\lor}{\vee} \newcommand{\land}{\wedge} \renewcommand{\phi}{\varphi} \renewcommand{\subset}{\subseteq} \newcommand{\models}{\vDash} \DeclareMathOperator{\dom}{Dom} \DeclareMathOperator{\ifp}{ifp} \DeclareMathOperator{\lfp}{lfp} \DeclareMathOperator{\gfp}{gfp} \DeclareMathOperator{\tcl}{tcl} \DeclareMathOperator{\ln}{ln} $

Będziemy tu omawiać twierdzenia Gödla – o zupełności, o niezupełności, o związkach z twierdzeniem o zwartości, twierdzeniem Turinga, itd.

Twierdzenie o zupełności

Ustalmy pewną skończoną sygnaturę. Niech $\Delta$ będzie teorią, to znaczy, zbiorem zdań, zwanych aksjomatami teorii $\Delta$. Jeżeli $M$ jest strukturą, to piszemy $M\models \Delta$ gdy $M$ spełnia wszystkie zdania z $\Delta$. Mówimy wtedy, że $M$ jest modelem teorii $\Delta$. Mówimy, że teoria $\Delta$ jest spełnialna, jeżeli istnieje przynajmniej jeden model tej teorii; w przeciwnym przypadku, mówimy że jest niespełnialna. Jeżeli $\phi$ jest zdaniem, to piszemy $\Delta\models \phi$ jeżeli każdy model teorii $\Delta$ spełnia zdanie $\phi$.

Przykład. Niech sygnatura zawiera symbol $\le$ oraz niech $\Delta$ zawiera 4 aksjomaty porządku liniowego. Wówczas $\Delta\not\models\phi$, gdzie $\phi$ jest zdaniem które mówi, że istnieje element najmniejszy, ponieważ istnieje model teorii $\Delta$ (czyli porządek liniowy) który nie posiada elementu najmniejszego. Natomiast $\Delta\models\psi$, gdzie $\psi$ jest zdaniem mówiącym, że jeśli są co najwyżej cztery elementy, to istnieje element największy. Istnieją zdania $\phi$ takie, że nie zachodzi ani $\Delta\models\phi$, ani $\Delta\models\neg\phi$. Na przykład, $\phi$ które mówi, że istnieją co najwyżej cztery elementy.

Powiemy, że teoria $\Delta$ jest zupełna, jeżeli jest spełnialna, ale każda większa teoria nie jest spełnialna (czyli $\Delta$ jest maksymalną spełnialną teorią). Na przykład teoria porządków liniowych nie jest zupełna, bo można jeszcze dodać aksjomat gęstości, i dostajemy większą, spełnialną teorię. Ale teoria gęstych porządków liniowych już jest zupełna. Tutaj dokonuję pewnego nieszkodliwego utożsamienia – dwie teorie $\Delta$ i $\Delta’$ uważam za równoważne, jeżeli mają dokładnie takie same modele. Tak więc, “teoria porządków liniowych” to jest teoria składająca się z czterech zdań, i równoważna teorii $\Delta’$ składającej się ze wszystkich zdań, które są prawdziwe we wszystkich porządkach liniowych.

Po dokonaniu tego typu utożsamienia, możemy powiedzieć równoważnie, że teoria jest zupełna, jeżeli dowolne dwa jej modele są nierozróżnialne za pomocą zdania logiki pierwszego rzędu.

Rzadko kiedy teoria $\Delta$ ma tylko jeden model (z dokładnością do izomorfizmu), nawet jeżeli teoria jest zupełna. Tak może być tylko w przypadku, gdy wszystkie modele teorii $\Delta$ mają tą samą, skończoną moc – to wynika z poniższego twierdzenia.

Twierdzenie (Skolem-Lowenheim). Jeżeli teoria $\Delta$ ma model nieskończony, to ma też model o dowolnej nieskończonej mocy $\mathfrak m$.

Systemy dowodowe

Istnieją różne systemy dowodowe dla logiki pierwszego rzędu, np. system Hilberta. Generalnie idea jest taka, by sformalizować pojęcie dowodu. Takie dowody zgrubsza odpowiadają temu, co matematycy robią pisząc dowody, z tą różnicą, że nie używają języka, lecz wyłącznie symboli, oraz mają bardzo precyzyjnie określone reguły dowodzenia. To, czy coś jest poprawnym dowodem powinno być sprawdzalne przez komputer.

Piszemy $\Delta\vdash\phi$, jeżeli istnieje formalny dowód $\phi$ z $\Delta$ (w jakimś ustalonym systemie dowodowym, np. Hilberta). $\Delta$ jest sprzeczna jeżeli $\Delta\vdash \bot$. Nietrudno pokazać, że jeśli $\Delta\vdash\phi$, to $\Delta\models\phi$ (ta implikacja nazywa się poprawnością systemu dowodowego). Twierdzenie o zupełności mówi o odwrotnej implikacji.

Twierdzenie o zupełności Gödla. Jeżeli $\Delta\models\phi$ to $\Delta\vdash\phi$. 

Z tego twierdzenia natychmiast wynikają następujące wnioski.

  • $\Delta\models\phi$ wtedy i tylko wtedy, gdy $\Delta\vdash\phi$.
  • Jeżeli teoria $\Delta$ jest niespełnialna to jest sprzeczna (i vice-versa).
  • Ogólniej, jeżeli teoria $\Delta\cup\set{\neg\phi}$ jest niespełnialna, to $\Delta\vdash\phi$, czyli z $\Delta$ da się udowodnić $\phi$ (w systemie dowodowym).
  • Twierdzenie o zwartości. Jeżeli teoria $\Delta$ jest niespełnialna, to niespełnialny jest pewien skończony zbiór zdań $\Delta_0\subset\Delta$. To wynika z tego, że dowód sprzeczności $\Delta\vdash\bot$ może tylko używać skończonej liczby zdań z $\Delta$.
  • Twierdzenie o zwartości, wariant II. Z każdego nieskończonego ciągu modeli można wybrać podciąg $\str M_1,\str M_2,\ldots$ elementarnie zbieżny do pewnego modelu $\str M^\ast$, w tym sensie, że dla dowolnego zdania $\phi$, $\str M^\ast\models \phi$ wtedy i tylko wtedy, gdy $M_n\models \phi$ dla dostatecznie dużych $n$. (ćwiczenie: pokazać równoważność dwóch wariantów tw. o zwartości). Dowód twierdzenia o zwartości, korzystający z ultrafiltrów zamiast z twierdzenia o zupełności, podany jest tutaj.

Teorie PA, ZFC

Oprócz prostych teorii, takich jak teoria porządków liniowych, teoria ciał, teoria grup, itd. istnieją także “skomplikowane” teorie, takie jak teorie PA i ZFC.

Teoria PA

Aksjomaty Arytmetyki Peano (Teoria PA) jest nad sygnaturą składającą się z unarnego symbolu $s$ oraz binarnych symboli $+,\cdot$, i symboli stałych $0,1$.

Aksjomaty tej teorii mówią o podstawowych własnościach arytmetycznych, oraz o indukcji matematycznej (w poniższych aksjomatach, zmienne wolne są implicite kwantyfikowane uniwersalne):

  1. $s$ jest funkcją różnowartościową: $x\neq y\implies s(x)\neq s(y)$ (formalnie, poprzedzamy to prefiksem $\forall x \forall y$, poniżej podobnie).
  2. $0$ nie ma poprzednika: $s(x)\neq 0$.
  3. $x+0=x$.
  4. Dodawanie a następnik: $s(x)+y=s(x+y)$
  5. $x\cdot 0=0$.
  6. Mnożenie a następnik: $s(x)\cdot y=x\cdot y+y$
  7. Aksjomat indukcji, ograniczony do własności definiowanych formułami z parametrami: $$(U(0)\land \forall x. U(x)\implies U(s(x))\\ \implies \forall x. U(x),$$ gdzie $U(x)$ jest dowolną formułą pierwszego rzędu z parametrami, tzn. $U(x)=\phi(x,u_1,\ldots,u_k)$ (formalnie, w powyższej formule, zamiast $U(x)$ wpisujemy $\phi(x,u_1,\ldots,u_k)$ oraz formułę tę poprzedzamy prefiksem $\forall u_1\ldots\forall u_k$).

Model Standardowy PA

Modelem standardowym teorii PA jest struktura $\mathcal N=(\mathbb N,s,+,\cdot,0,1)$, gdzie $\mathbb N$ są liczbami naturalnymi (najmniejszy taki zbiór, że $\emptyset\in\mathbb N\land \forall n\in\mathbb N.n\cup\set{n}\in\mathbb N$. Taki zbiór istnieje, na mocy aksjomatów ZFC, którymi się posługujemy na codzień. Interpretacją funkcji $s$ jest $s=\lambda n.n\cup\set{n}$, dodawanie i mnożenie są zdefiniowane przez indukcję jak zazwyczaj.

Modele niestandardowe PA

Na mocy twierdzenia Skolema-Lowenheima, teoria PA, ponieważ jest spełnialna, to ma modele dowolnej mocy nieprzeliczalnej. To są przykłady modeli niestandardowych teorii PA. Poniżej opiszemy inną konstrukcję modeli niestandardowych. Jeszcze inna konstrukcja opisana jest tutaj.

Rozważmy sygnaturę $\Sigma$ składającą się z symboli $+,\cdot,s,0,1$ oraz, dodatkowo, z symbolu stałej $K$. Dla $k=0,1,2,\ldots$, niech $\mathcal N_k$ oznacza model standardowy $\mathcal N$, uzupełniony o interpretację stałej $K$, przyjmującej wartość $k\in\mathcal N$. A zatem, zdefiniowaliśmy ciąg struktur $\mathcal N_0,\mathcal N_1,\mathcal N_2,\ldots$ nad sygnaturą $\Sigma$, i na mocy drugiego wariantu twierdzenia o zwartości (zob. wyżej), ten ciąg struktur posiada podciąg zbieżny elementarnie do pewnej struktury $\mathcal N^*$.

Ponieważ każda ze struktur $\mathcal N_k$ spełnia każdy z aksjomatów PA, wynika stąd, że także struktura $\mathcal N^*$ także je spełnia, więc jest to model teorii PA. Ta struktura nie musi mieć jako nośnika zbioru liczb naturalnych, tym bardziej interpretacja funkcji $+,\cdot,s$ nie musi być taka, jak w modelu standardowym.

W strukturze $\mathcal N^*$ spełnione jest zdanie $K>0$ (ponieważ zachodzi ono w $\mathcal N_k$ dla $k>0$), także spełnione jest zdanie $K>s(0)$ (ponieważ zachodzi w $\mathcal N_k$ dla $k>1$) itd., $K>s^n(0)$ dla dowolnej liczby $n\in\mathbb N$ – fenomen, który nie występuje w modelu standardowym (oczywiście, nie zachodzi $K>x$ dla dowolnego elementu $x\in\mathcal N$).  Natomiast większość twierdzeń arytmetyki, takie jak małe twierdzenie Fermata (wielkie być może też), twierdzenie chińskie o resztach, itd., zachodzą w modelu $\mathcal N^*$, ponieważ są to twierdzenia teorii PA.

Teoria ZFC

Ustalmy sygnaturę składającą się z jednego symbolu binarnego, $\in$. Teoria ZFC ma nieskończenie wiele aksjomatów. Przykładowe aksjomaty to:

  • Aksjomat ekstensjonalności: $\forall x\forall y.(\forall z. z\in x\iff z\in y)\implies x=y$
  • Aksjomat wyboru: każda relacja równoważności $\sim\subset X\times X$ ma funkcję wyboru $f:X/\sim \to X$ t.że $f(c)\in c$ dla $c\in X/sim$.
  • Niech $x\subseteq y$ będzie skrótem notacyjnym dla formuły $\forall z.z\in x\implies z\in y$. Aksjomat zbioru potęgowego: $\forall x\exists y.\forall z. z\in y\iff z\subseteq x$. (Zbiór $y$ gwarantowany przez aksjomat oznaczamy $P(x)$).
  • Niech $s(n)$ będzie skrótem notacyjnym dla $n\cup\set{n}$. Aksjomat nieskończoności: $$\exists N.\emptyset\in N\land \forall n\in N s(n)\in N.$$ (Najmniejszy zbiór $N$ spełniający tę własność oznaczamy przez $\mathbb N$).
  • Niech $\phi$ będzie formułą z jedną zmienną wolną. Aksjomat wycinania przy pomocy formuły $\phi$: $$\forall x\exists y. \forall z. z\in y\iff z\in x\land \phi(x).$$ (Zbiór $y$ gwarantowany przez aksjomat oznaczamy $\set{z\in x:\phi(x)}$. Aksjomatów wycinania jest nieskończenie wiele, po jednym dla każdej formuły, więc mówi się o schemacie. 
  • Itd.

Teoria ZFC, o ile ma jakiś model, to ma tych modeli wiele – to wynika z twierdzenia Skolema-Lowenheima. Także, ma wtedy model przeliczalny, co może wydawać się niezgodne z intuicją, że model teorii ZFC powinien mieć np. przynajmniej continuum elementów, żeby pomieścić np. wszystkie liczby rzeczywiste. Wytłumaczenie tego paradoksu jest następujące. Model teorii ZFC jest to po prostu struktura $M$ nad sygnaturą $\set{\in}$, którą konstruujemy wewnątrz naszego uniwersum matematycznego; nazywamy ten model $M$ modelem wewnętrznym. Nie musimy (a nawet nie możemy) używać do tego celu wszystkich elementów naszego uniwersum; jego nośnik musi mieć jakąś określoną moc. Ale za to interpretację relacji $\in$ możemy zdefiniować w dowolny sposób. Żeby skonstruować przeliczalny model wewnętrzny, możemy np. zadeklarować, że elementami modelu $M$ są te formuły matematyczne nad sygnaturą $\set{\in}$ z jedną zmienną wolną $x$, które są spełnione dla dokładnie jednego zbioru $x$ w naszym uniwersum (takich formuł jest przeliczalnie wiele). Np. zbiór pusty odpowiada wtedy formule $\forall y.y\notin x$, a zbiór liczb rzeczywistych odpowiada formule $\forall y.y\subset\mathbb N\iff y\in x$ (gdzie $\mathbb N$ to jest skrót notacyjny na zbiór opisany w aksjomacie indukcji). Warto by te formuły utożsamić przy pomocy pewnej relacji równoważności: $\phi\sim \psi$ wtw. gdy  $\forall x.\phi(x)\iff\psi(x)$. Natomiast piszemy $\phi\in\psi$ jeżeli $\forall x,y.\phi(x)\land\psi(y)\implies (x\in y).$ To, co właśnie opisaliśmy to jest pewna przeliczalna struktura nad sygnaturą $\set{\in}$, która być może jest modelem dla ZFC (nie wiem, czy jest).

Twierdzenie o niezupełności

Nie jest zaskoczeniem, że są teorie, które nie są zupełne, np. teoria porządków liniowych. Co może jednak być zaskoczeniem jest to, że ZFC nie jest teorią zupełną – to mówi twierdzenia Gödla o niezupełności. Co za tym idzie, są twierdzenia (zdania) $\phi$ takie, że ani $\phi$, ani $\neg \phi$ nie dadzą się udowodnić (w ZFC). Okazuje się że takie zdania istnieją, chyba, że zachodzi jeszcze gorszy scenariusz – że teoria ZFC jest sprzeczna (wtedy wszystko da się udowodnić). Tego drugiego scenariusza nie da się wykluczyć (tj. udowodnić w ZFC, że nie zachodzi)  – to mówi drugie twierdzenie Gödla o niezupełności. Ponadto, oba te scenariusze zachodzą nie tylko dla ZFC, ale też dla dowolnej innej rozsądnej teorii która jest w stanie mówić o liczbach naturalnych (np. ZF, ZFC+hipoteza continuum). Oba te twierdzenia stosunkowo łatwo udowodnić, korzystając z pojęcia maszyny Turinga.

Zamiast mówić o maszynach Turinga, dla uproszczenia będę mówił o programach komputerowych (w ustalonym języku, np. C++, Java, Python, OCaml, itd.).

Powiemy, że program $P$ się zatrzymuje, jeżeli po jego uruchomieniu bez żadnego argumentu, program w pewnym momencie kończy działanie.

Funkcja Halt to funkcja, która przyjmuje jako argument program  $P$ oraz w wyniku zwraca $1$ jeśli $P$ się zatrzymuje, i zwraca $0$ w przeciwnym przypadku.

Twierdzenie Turinga. Nie istnieje program który oblicza funkcję Halt.

Rozważmy następującego kandydata na program obliczający funkcję Halt. Program Hilbert, dostawszy na wejściu program $P$, enumeruje wszystkie poprawne dowody w systemie Hilberta tak długo, aż napotka dowód, że program $P$ się zatrzymuje – wtedy zwraca $1$ – bądź dowód, że program $P$ się nie zatrzymuje – wtedy zwraca $0$.

[Stwierdzenie “program P się zatrzymuje” da się opisać formułą w ZFC: należy opisać semantykę języka programowania. To się robi dokładnie tak, jak na zajęciach z semantyki – używa się tam przecież ZFC. Łatwiej, gdy nasz “język” programowania to maszyny Turinga – wtedy semantykę się opisuje (też w ZFC) po prostu mówiąc, że istnieje bieg akceptujący (bieg to jest ciąg konfiguracji, bla bla bla, ale to są obiekty ZFC).

Trudniej jest, jeśli powyżej, zamiast o ZFC, mówimy o aksjomatach Peano (PA), bo nie jest to teoria zbiorów, lecz teoria arytmetyczna. Teoria PA jest równoważna (w pewnym prostym sensie) teorii ZFC–Inf, czyli teorii ZFC z zaprzeczeniem aksjomatu indukcji. Jest to teoria zbiorów, i można mówić o maszynach Turinga, ich biegach itd. oraz o semantyce większości języków programowania. Natomiast funkcja $\beta$ jest potrzebna żeby pokazać, jak ZFC–Inf koduje się w PA.]

Na mocy twierdzenia Turinga, program Hilbert nie oblicza funkcji Halt. A to znaczy, że istnieje argument – pewien program $P$ – dla której wynik $Hilbert(P)$ jest nieokreślony, bądź jest różny od $Halt(P)$.

Druga możliwość jest niemożliwa, bo jeśli istnieje dowód, że $P$ się zatrzymuje (bądź nie), to znaczy, że $P$ tak faktycznie robi (o ile ZFC jest niesprzeczne).

Wniosek. Istnieje program $P$ dla którego nie istnieje dowód (w ZFC), że się zatrzymuje, ani nie istnieje dowód, że się nie zatrzymuje.

Jako natychmiastowy wniosek otrzymujemy pewien wariant pierwszego twierdzenia Gödla o niezupełności.

Twierdzenie o niezupełności Gödla (słaby wariant). Jeśli ZFC jest niesprzeczne, to istnieje twierdzenie matematyczne $\phi$ (formuła w języku ZFC) takie, że $\textrm{ZFC}\not\vdash \phi$ oraz $\textrm{ZFC}\not\vdash \neg\phi$.

Przykładowe stwierdzenie, o którym wiadomo, że nie da się go ani udowodnić, ani obalić w ZFC, to słynna Hipoteza Continuum (CH): że $\mathfrak c$ jest najmniejszą nieprzeliczalną liczbą kardynalną. Da się udowodnić (w ZFC!), że CH nie da się ani obalić, ani udowodnić (w ZFC). To się robi tak, że się konstruuje dwa (przeliczalne) modele ZFC, z których jeden spełnia CH, a drugi spełnia ¬CH. Czyli zarówno ZFC+CH, jak i ZFC+¬CH są niesprzeczne (pod warunkiem, że ZFC jest niesprzeczne; jeśli ZFC jest sprzeczne, to wszystkie te dywagacje są próżne).

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>