logika dokazivosti

Goedelovi teoremi nepotpunosti -- 90 godina poslije

Mladen Vuković i Petar Gregorek
 



Sažetak

Proteklo je 90 godina od kako je Kurt Goedel objavio svoje teoreme nepotpunosti. U ovom članku namjera nam je opisno izreći te teoreme i komentirati neke ideje Goedelovog dokaza. Zatim ćemo razmatrati jedan rezultat o prirodnim brojevima koji nije dokaziv u Peanovoj aritmetici. Na kraju ćemo istaknuti neka današnja istraživanja o dokazivosti u matematičkim teorijama koja su potaknuta Goedelovim teoremima nepotpunosti.



Ključne riječi

Peanova aritmetika, Goedelovi teoremi nepotpunosti, aritmetizacija, Goodsteinov teorem, logika dokazivosti



1Kratka biografija Kurta Goedela

Ovdje ćemo navesti vrlo kratku biografiju Kurta Goedela. Daleko više detalja možete pronaći u [13]. Kurt Goedel rođen je 28. travnja 1906. u Bruennu koji je bio središte tadašnje austro-ugarske pokrajine Moravske (to je današnje Brno u češkoj Republici). Studirao je matematiku na Bečkom sveučilištu, a 1930. godine je obranio doktorsku disertaciju i postao profesorom na istom sveučilištu. Mentor disertacije je bio Hans Hahn (iz Hahn–Banachovog teorema). U disertaciji je dokazao značajan teorem o potpunosti logike prvog reda. Važan događaj u Goedelovom životu bio je prisustvovanje Hilbertovom predavanju u Bologni o potpunosti i konzistentnosti matematičkih teorija. Godine 1931. objavio je članak o nepotpunosti aritmetike gdje su dokazana dva teorema koji se obično nazivaju Goedelov prvi i drugi teorem nepotpunosti. Nakon što je nacistička Njemačka pripojila Austriju Goedel je 1940. godine emigrirao u SAD. Te godine je objavio drugi svoj jako značajan rezultat. Radi se o dokazu konzistentnosti aksioma izbora i generalizirane hipoteze kontinuuma sa Zermelo–Fraenkeolovom teorijom skupova.1 Postao je stalni član Institute for Advanced Study u Princetonu 1946. godine. često se družio s Albertom Einsteinom koji je znao reći da dolazi na Institut kako bi imao privilegiju šetati i razgovarati s Goedelom. Godine 1951. Goedel je pokazao egzistenciju paradoksalnih rješenja Einsteinovih jednadžbi polja u općoj teoriji relativnosti. Njegova rješenja se nazivaju Goedelova metrika. Iste godine mu je dodijeljena nagrada Albert Einstein (bio je prvi dobitnik nagrade). Redoviti profesor na Institute for Advanced Study u Princetonu postao je 1953. godine. Vrlo prestižnu nagradu National Medal of Science, koju dodjeljuje predsjednik SAD-a, primio je 1974. godine. Sve do svoje smrti 14. siječnja 1978. radio je na Institutu u Princetonu.





Kurt Goedel i Albert Einstein


2Goedelovi teoremi nepotpunosti

Oba Goedelova teorema nepotpunosti govore da neke tvrdnje o prirodnim brojevima nisu dokazive u Peanovoj aritmetici (skraćeno PA). Budući da ovdje nećemo dokazivati Goedelove teoreme, onda nećemo ni navoditi aksiome sistema PA (primjerice, u [19] definirana je detaljno teorija PA). Ovdje ćemo vrlo neformalno izreći Goedelove teoreme nepotpunosti. No kako bi iskazi teorema bili jasniji moramo ipak reći nekoliko riječi o teoriji PA. Osnovni simboli od kojih gradimo izraze u teoriji PA sadržani su u sljedećem skupu:
\lbrace \neg, \ \rightarrow, \forall, =,\ ', +, \cdot \ , 0, (, )\rbrace \cup \lbrace x_{k} : k\in {\mathbb{N}} \rbrace .
Elementi prvog skupa su redom: logički simboli (\neg se naziva veznik negacije, simbol \rightarrow se naziva kondicional, a \forall je univerzalni kvantifikator), relacijski dvomjesni simbol = (standradna interpretacija ovog simbola je, naravno, relacija jednakosti), funkcijski jednomjesni simbol ' i dvomjesni funkcijski simboli + i \cdot, konstantski simboli 0 te zagrade. Elementi drugog skupa se nazivaju individualne varijable. Skup osnovnih simbola se obično naziva alfabet.

Nadamo se da vam je jasna standardna interpretacija funkcijskog simbola + i \cdot. Jednomjesni funkcijski simbol ' se standardno interpretira funkcijom f:{\mathbb{N}} \to {\mathbb{N}} koja je zadana s f(n)=n+1. Standardna interpretacija konstatskog simbola je prirodan broj nula.

Model teorije PA u kojoj su svi simboli interpretirani na standardni način naziva se {\it standardni model}. Ostali modeli teorije PA koji nisu izomorfni standardnom modelu nazivaju se {\it nestandardni modeli}.

Primjenom simbola alfabeta možemo graditi razne izraze. Najvažnije izraze nazivamo formule. Primjerice, izrazi \forall x_{3}( x_{1}+x_{20}= x_{3} \cdot x_{5}'') \rightarrow \neg \forall x_{4} \neg (x_{4}\cdot x_{1}=0'')  i  \forall x_{2} \neg \forall x_{1} \neg (x_{2}'''=x_{1}\cdot x_{1} +0'') su primjeri dviju formula teorije PA. Ako su u formuli sve varijable vezane nekim kvantifikatorima tada takvu formulu nazivamo rečenica. U prethodno navedenim primjerima prva formula nije rečenica, a druga jeste.

Pojam {\it istinitosti neke formule na standardnom modelu} se formalno definira u matematičkoj logici. Ovdje nećemo navoditi tu definiciju. No pokušat ćemo objasniti razliku između pojmova istinitosti i {\it dokazivosti neke formule u teoriji} PA. Glavno je pitanje, po našem skromnom mišljenju, na koji način se utvrđuje istinitost neke formule teorije PA. To nije strogo definirano. Koliko je to teško pitanje navest ćemo jedan primjer koji navodi američki časopis Notices (vidi [1]). Postavljen je problem mogu li se za svaki prirodan broj n svi brojevi iz skupa \lbrace 1,2, \ldots,n\rbrace obojati s tri boje tako da niti jedna Pitagorina trojka (tj. trojke prirodnih brojeva a,b,c za koje vrijedi a^{2} + b^{2}=c^{2}) iz tog skupa nisu obojane istom bojom. Primjenom računala dokazano je da za broj n=7 824 takvo bojanje postoji (štoviše, određeno je jedno traženo bojanje). Zatim, je primjenom računala dan dokaz veličine 200 terabajta da za broj n=7 825 traženo bojanje ne postoji (često se zna reći da je to najduži dokaz koji je ikad pronađen). Mi ćemo u ovom članku gdje god je to moguće radije pisati da se radi o nekom rezultatu iz teorije brojeva kako se ne bi upuštali u raspravu na koji način je dokazana istinitost neke formule na standardnom modelu.

Ako neka rečenica F nije istinita na standardnom modelu, tada je nužno istinita negacija te rečenice, tj. \neg F, na standardnom modelu. To znači da za svaku rečenicu vrijedi da je ona istinita ili je njena negacija istinita na standardnom modelu.

Pojam dokaza u teoriji PA se strogo definira kao konačan niz formula s određenim svojstvima (vidi [19]). Ako je F formula koja je dokaziva u teoriji PA tada to označavamo s \textsf{PA}\vdash F. Kažemo da je teorija PA konzistentna ako u njoj nije moguće istovremeno dokazati neku formulu i negaciju te formule, tj. ne postoji formula F tako da imamo \textsf{PA}\vdash F  i  \textsf{PA}\vdash \neg F.



Prvi Goedelov teorem nepotpunosti
Ako pretpostavimo da je teorija PA konzistentna tada je ona nepotpuna, tj. postoji rečenicaG tako da vrijedi} PA \not\vdash G   i  PA \not\vdash \neg G.


Rečenica G, čija egzistencija se tvrdi u prethodnom teoremu, naziva se Goedelova rečenica. Istaknimo odmah neposrednu posljedicu Goedelovog prvog teorema. Bili smo napomenuli da za svaku rečenicu F vrijedi da je ona ili pak formula \neg F istinita na standardom modelu. Posebno to vrijedi za Goedelovu rečenicu. Time smo dobili sljedeći rezultat:



U teoriji PA nije moguće dokazati svaku istinitu rečenicu, odnosno istinitost nije isto što i dokazivost.


U prvi tren mogli bi reći da to samo znači da smo loše odabrali aksiome teorije PA. No iz dokaza Goedelovog prvog teorema može se vidjeti da teorem vrijedi i za proširenja od PA. Znači, ako bi dodali neke nove aksiome opet je moguće konstruirati neku rečenicu tako da niti ona, a ni njena negacija nisu dokazive. Iz toga slijedi da niti jedna matematička teorija koja sadrži PA nije potpuna. Goedelov prvi teorem nepotpunosti zapravo ističe ograničenja aksiomatske metode.

Prirodno se postavlja pitanje kako glasi rečenica G, odnosno koje to svojstvo prirodnih brojeva nije dokazivo u PA. Opet, jako neformalno i neprecizno govoreći, intutivni opis Goedelove rečenice glasi "Ova rečenica nije dokaziva". Vjerojatno ćete se začuditi i odmah pomisliti da to baš i nije neko svojstvo prirodnih brojeva zbog kojeg bismo se trebali brinuti što nije dokazivo u teoriji PA. To je čak dugo vrijeme (preko trideset godina) bio argument o ne prevelikoj važnosti Goedelovog prvog teorema nepotpunosti. No sedamdesetih godina prošlog stoljeća J. Paris i L. Harrington su prvi otkrili neke kombinatorne principe o prirodnim brojevima koji nisu dokazivi u teoriji PA. Neke istaknute rezultate o prirodnim brojevima koji nisu dokazivi u teoriji PA razmatrat ćemo malo kasnije.

Kao mali uvod za drugi Goedelov teorem nepotpunosti, reći ćemo nekoliko riječi o Hilbertovom programu. Na drugom svjetskom matematičkom kongresu 1900. godine u Parizu veliki njemački matematičar David Hilbert (1862.-1943.) istaknuo je 23 problema iz raznih područja matematike, čije je rješavanje pridonijelo velikom razvoju matematike u XX. stoljeću. Neki od tih problema pripadaju matematičkoj logici. Drugi Hilbertov problem jednostavno glasi ovako: Dokazati konzistentnost aritmetike. Nakon otkrivenih paradoksa u teoriji skupova pitanje konzistentnosti matematičkih teorija postalo je jako značajno. Hilbert je želio da se točno odrede dijelovi matematike u kojima se svi dokazi mogu izvršiti na formalan (i konačan) način, odnosno da se naglase dijelovi gdje su mogući problemi. Svrha velikog i ambicioznog Hilbertovog programa bila je postaviti aksiomatske osnove na kojima bi se moglo temeljiti svako istraživanje u matematici. No upravo je sljedeći teorem pokopao nade u ostvarenje Hilbertovog programa. Prije iskaza teorema želimo još naglasiti da je u teoriji PA moguće konstruirati rečenicu Con_{PA} koja izriče konzistentnost te teorije.



Drugi Goedelov teorem nepotpunosti
Ako je teorija PA konzistentna tada rečenica Con_{PA} nije dokaziva u toj teoriji.




3Aritmetizacija

Koliko su važni sami Goedelovi teoremi, usuđujemo se reći da su za razvoj matematičke logike jednako važne i ideje i metode koje je Goedel koristio prilikom dokaza svojih teorema nepotpunosti. Obično se Goedelov dokaz dijeli na tri velika dijela: aritmetizacija, reprezentabilnost i dijagonalizacija. Ovdje ćemo posebno istaknuti ideju aritmetizacije. Ideja aritmetizacije u matematičkoj logici analogna je Descartesovoj ideji preslikavanja geometrije u algebru, tj. analitičkoj geometriji.

Sjetimo se, primjerice, kako u analitičkoj geometriji provjeravamo paralelnost pravaca u ravnini koji su zadani svojim eksplicitnim jednadžbama: jednostavno provjerimo imaju li jednake koeficijente smjera. želimo naglasiti da ne moramo crtati pravce u koordinatnom sustavu i uvjeriti se jesu li paralelni. Slično je postupio Goedel s formulama i dokazima teorije PA.

Označimo s g funkciju koju prvo definiramo za svaki simbol alfabeta teorije PA na sljedeći način:



g(( ) =2, g()) =3, (funkcija g lijevoj zagradi pridružuje broj 2, a desnoj 3)
       
g\big( \neg\big) =5, g\big( \rightarrow \big) =7, g\big( \forall\big) =11, g\big( =\big) =13,
       
g\big( 0\big) =17, g\big( '\big) =19, g\big( +\big) =23, g\big( \cdot \big) =29,
       
g\big( x_{k}\big)=31+k, za svaki k\in {\mathbb{N}}.

Sada se funkcija g proširuje ne samo na skup svih formula ve\' c i na skup svih dokaza u Peanovoj aritmetici. Ako je  e_{0} e_{1}\ldots e_{r}  neki izraz u Peanovoj aritmetici (formula ili dokaz) tada vrijednost funkcije g na tom izrazu definiramo sa:

2^{g(e_{0})}\cdot 3^{g(e_{1})}\cdot \ldots \cdot p_{r}^{g(e_{r})},
gdje je p_{i}i-ti po redu prosti broj. Tako, primjerice, aksiomu teorije PA koji glasi \forall x_{1}(x_{1}+0=x_{1}) funkcija g pridružuje prirodni broj

2^{g(\forall)} \cdot 3^{g(x_{1})}\cdot 5^{g(()}\cdot 7^{g(x_{1})}\cdot 11^{g(+)}\cdot 13^{g(0)} \cdot 17^{g(=)}\cdot 19^{g(x_{1})} \cdot 23^{g())},
tj. broj 2^{11} \cdot 3^{32}\cdot 5^{2}\cdot 7^{32}\cdot 11^{23}\cdot 13^{17} \cdot 17^{13}\cdot 19^{32} \cdot 23^{3}.

Uočite da je tako definirana funkcija g injekcija. Ako je s neki simbol ili izraz tada vrijednost g(s) nazivamo Goedelov broj od s.

Primjenom aritmetizacije Goedel je preveo probleme o Peanovoj aritmetici na probleme s prirodnim brojevima. Goedelu u čast aritmetizacija se naziva i gedelizacija. Ako je F neka formula te n=g(F), tada s \lceil F \rceil označavamo sljedeći izraz:

0\overbrace{'' ... '''}^{n}
te ga nazivamo numeral pridružen formuli F. Koristeći aritmetizaciju može se definirati formula Pr(x) koja se naziva predikat dokazivosti. Istaknimo ovdje samo jedno svojstvo predikata dokazivosti: formula \neg Pr(\lceil G\rceil)\leftrightarrow G je dokaziva u teoriji PA (kaže se još da je Goedelova rečenica G fiksna točka predikata \neg Pr.) U daljnjim razmatranjima istaknuti ćemo još neka svojstva predikata dokazivosti Pr.

Skice dokaza teorema nepotpunosti nalaze se u više članaka i knjiga na hrvatskom jeziku ([15], [7], [17], ...). Sigurno je za prvo čitanje bolje pogledati skicu dokaza, a ne se odmah upustiti u detaljno raspisivanje. Nerijetko se može čuti da je K. Goedel bio "vrhunski programer" bez obzira što početkom prošlog stoljeća nisu postajala računala. Time se, zapravo, želi reći da je orginalni Goedelov dokaz sličan kodu nekog programa za računalo. Zahvaljujući V. G. Kirinu u [7] možete pregledati hrvatski prijevod Goedelovog orginalnog članka. Vrlo detaljne dokaze Goedelovih teorema nepotpunosti na hrvatskom jeziku možete pogledati u [20] i [8].



4Neki rezultati iz teorije brojeva koji nisu dokazivi u teoriji PA

Bili smo naveli da se na prvi pogled Goedelova rečenica G čini jako umjetna i nezanimljiva tvrdnja o prirodnim brojevima. U ovom dijelu opisat ćemo detaljnije jedan zanimljiv (nadamo se da ćete se složiti da je zanimljiv kada ga pročitate) rezultat iz teorije brojeva koji nije dokaziv u teoriji PA.

Tvrdnja teorema kojeg razmatramo u ovoj točki je pomalo čudna na prvi pogled, čak izgleda nevjerojatna. Kako bi mogli izreći teorem moramo prvo definirati prikaz prirodnog broja u superbazi te onda definirati Goodsteinov niz prirodnog broja. Te pojmove nećemo strogo definirati već ćemo ih objasniti pomoću primjera.

Sigurno vam je poznat pojam prikaza broja u nekoj bazi. Primjerice, prikaz broja 521 u bazi 2 izgleda ovako: 521= 2^{9} + 2^{3} +2^{0}.

Prikazati neki broj u superbazi b znači prvo broj prikazati u bazi b, zatim eksponente prikazati u bazi b, pa eksponente eksponenata prikazati u bazi b, itd. Pogledajmo to na primjeru prikaza broja 521 u superbazi 2:
521 = 2^{9} + 2^{3} +2^{0} = 2^{2^{3} +1 } + 2^{2+1}+2^{0} = 2^{2^{2+1}+1 } + 2^{2+1}+2^{0}
Dakle, prikaz broja 521 u supebazi 2 izgleda 2^{2^{2+1}+1 } + 2^{2+1}+2^{0}. Ovdje je kao primjer dan i prikaz broja 521 u superbazi 3:
521 = 2\cdot 3^{5} +3^{3} +2\cdot 3+2 = 2\cdot 3^{3+2}+3^{3}+ 2\cdot 3 + 2
Dakle, prikaz broja 521 u supebazi 3 izgleda 2\cdot 3^{3+2}+3^{3}+ 2\cdot 3 + 2.

Sada ćemo prvo opisati postupak kako odrediti nekoliko prvih članova Goodsteinovog niza broja 8. Prvi član Goodsteinovog niza broja 8 je on sam. Označavamo ga s (8)_{1}=8. Kako bi dobili drugi član niza prikažimo prvo broj 8 u superbazi 2, tj. 8=2^{2+1}. Umjesto svih dvojki u prikazu 2^{2+1} napišemo trojke, pa dobivamo 3^{3+1}. Zatim od tako dobivenog broja oduzmemo 1. Time smo dobili drugi član Goodsteinovog niza, tj. (8)_{2}=80. Prikažimo sada broj 80 u superbazi 3, zatim zamijenimo sve trojke četvorkama te oduzmemo jedan. Dobili smo (8)_{3}=553. Nadamo se da je jasan daljnji postupak konstrukcije Goodsteinovog niza. Bez daljnjih detaljnih objašnjena navodimo nekoliko prvih članova Goodsteinovog niza broja 8.
\begin{array}{lrl} & (8)_{1} = & 8 \\ \text{}\\ {\small superbaza} \ 2 & & 8 = 2^{2+1}\\ 2\mapsto 3 & & \text{}\hskip 2em 3^{3+1}= 81 \\ -1 & (8)_{2} = & 80 \\ \text{}\\ {\small superbaza} \ 3 & & 80 = 2\cdot 3^{3} + 2\cdot 3^{2} + 2\cdot 3 +2 \\ 3\mapsto 4 & & \text{}\hskip 2.4em 2\cdot 4^{4} + 2\cdot 4^{2} + 2\cdot 4 +2 = 554 \\ -1 & (8)_{3} = & 553 \\ \text{}\\ {\small superbaza} \ 4 & & 553 = 2\cdot 4^{4} + 2\cdot 4^{2} + 2\cdot 4 +1 \\ 4\mapsto 5 & & \text{}\hskip 2.8em 2\cdot 5^{5} + 2\cdot 5^{2} +2\cdot 5 +1 = 6\ 311 \\ -1 & (8)_{4} = & 6\ 310 \\ \text{}\\ {\small superbaza } \ 5 & & 6\ 310 = 2\cdot 5^{5} + 2\cdot 5^{2} + 2\cdot 5 \\ 5\mapsto 6 & & \text{}\hskip 3.8em 2\cdot 6^{6} + 2\cdot 6^{2} + 2\cdot 6 = 93 \ 396 \\ -1 & (8)_{5} = & 93\ 395 \\ \text{}\\ {\small superbaza} \ 6 & & 93\ 395 = 2\cdot 6^{6} +2\cdot 6^{2} + 6 + 5\\ &\vdots \\ & (8)_{6} = & 1 \ 647 \ 195 \\ & (8)_{7}= & 33\ 554\ 571 \\ & (8)_{8}= & 774\ 841 \ 151 \\ & (8)_{9}= & 20\ 000\ 000\ 211 \\ & (8)_{10}=& 570\ 623\ 341\ 475 \\ & \vdots & \end{array}

Sada navodimo nekoliko prvih članova Goodsteinovog niza broja 25.
\begin{array}{rl} (25)_{1}=25 & = 2^{2^{2}} + 2^{2+1} +1\\ & \\ & \text{}\hskip 1em 3^{3^{3}} + 3^{3+1} + 1 \\ & \\ (25)_{2} & = 3^{3^{3}} + 3^{3+1} \approx 10^{13}\\ & \\ & \text{}\hskip 1em 4^{4^{4}} + 4^{4+1} \\ & \\ (25)_{3} & = 4^{4^{4}} + 3\cdot 4^{4} + 3\cdot 4^{3} + 3\cdot 4^{2} + 3\cdot 4 +3 \approx 10^{81} \\ & \\ & \text{}\hskip 1em 5^{5^{5}} + 3\cdot 5^{5} + 3\cdot 5^{3} + 3\cdot 5^{2} + 3\cdot 5 +3\\ & \\ (25)_{4} & = 5^{5^{5}} + 3\cdot 5^{5}+ 3\cdot 5^{3} + 3\cdot 5^{2} + 3\cdot 5 +2\approx10^{2\; 216}. \end{array}

Najvjerojatnije ste zaključili da Goodsteinovi nizovi brojeva 8 i 25 teže prema beskonačnosti (jeste li?). Ako jeste, prevarili ste se. R. L. Goodstein je dokazao 1944. godine da svaki Goodsteinov niz završava s nulom. Kako je to moguće? U prvi tren se čini nevjerojatno. Više primjera u vezi Goodsteinovog teorema možete pogledati u [18].

Detaljan dokaz Goodsteinovog teorema možete pogledati u [21] gdje se koristi transfinitna indukcija do ordinalnog broja \epsilon_{0}. Uobičajena matematička indukcija je zapravo transfinitna indukcija do ordinalnog broja \omega.

Budući da Goodsteinov teorem govori o prirodnim brojevima, prirodno se nameće pitanje može li se provesti dokaz tog teorema u kojem se neće koristiti beskonačni ordinalni brojevi. Godine 1982. je dokazano da se Goodsteinov teorem ne može dokazati u teoriji PA.

U diplomskom radu [6] razmatrano je nekoliko rezultata iz kombinatorike koji su nedokazivi u teoriji PA. To su razne verzije Ramseyevog teorema, zatim Heraklo i hidra, bitka s crvom, Kruskalov teorem o konačnim stablima i Friedamanov teorem. U [6] dan je i dokaz Paris–Harringtonovog teorema u kojem se tvrdi da Ramseyev teorem za relativno velike skupove nije dokaziv u teoriji PA.



5Neka današnja istraživanja u vezi Goedelovih teorema

U ovom dijelu navest ćemo osnovne informacije o logikama dokazivosti i neke detalje o logikama interpretabilnosti. Glavni razlog uvrštavanja ovih tema je činjenica da se u Zagrebu provode istraživanja vezana uz njih. U [4] možete pronaći razne druge teme koje su povezane s Goedelovim teoremima a u vezi kojih se u današnje vrijeme provode istraživanja.

Prvo ćemo pokušati objasniti motivaciju za razmatranja logika dokazivosti. Prilikom proučavanja dokaza Goedelovih teorema nepotpunosti istaknuta su neka posebna svojstva predikata dokazivosti Pr. To su tzv. Hilbert–Bernaysovi uvjeti dokazivosti. Još je Goedel uočio da bi trebala postojati veza s modalnim logikama jer u normalnim modalnim sistemima postoje analogoni.2 Ovdje navodimo istaknuta svojstva predikata dokazivosti i analogone u modalnoj logici.
\begin{array}{lcl} \text{Hilbert–Bernaysovi uvjeti dokazivosti} & & \text{Normalne modalne logike}\\ \text{}\\ Pr(\lceil A\rightarrow B\rceil)\rightarrow (Pr(\lceil A\rceil)\rightarrow Pr(\lceil B\rceil)) & \text{}\hskip 1em\text{} & \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)\\ \text{}\\ Pr(\lceil A\rceil)\rightarrow Pr ( \lceil Pr(\lceil A\rceil)\rceil) & & \Box A\rightarrow \Box \Box A\\ \text{}\\ \text{ako } \textsf{PA}\vdash A \text{ tada } \textsf{PA}\vdash Pr (\lceil A\rceil) & & \text{ ako } \vdash A \text{ tada } \vdash \Box A \end{array}

Ključni korak u povezivanju svojstva predikata dokazivosti s modalnim logikama dogodio se Loebovim rješenjem Henkinovog problema, tj. rješenjem pitanja o dokazivosti fiksne točke predikata Pr (prisjetimo se da je Goedelova rečenica fiksna točka predikata \neg Pr; Henkinova rečenica H je fiksna točka predikata Pr, tj. vrijedi PA \vdash Pr(\lceil H\rceil) \leftrightarrow H).

Sada ćemo navesti osnovne definicije te istaknuti najvažnije činjenice o logici dokazivosti GL (Goedel–Loeb). Više detalja možete pronaći u [3] i [9].

Alfabet logike dokazivosti GL sadrži sve simbole logike sudova te jedan unarni modalni operator \Box. Pojam formule se definira standardno. Logika dokazivosti GL sadrži sljedeće aksiome:



\bullet [(A0)] sve tautologije logike sudova (ali u modalnom jeziku)
\bullet [(A1)] \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)
\bullet [(A2)] \Box A\rightarrow \Box \Box A
\bullet [(A3)] \Box (\Box A \rightarrow A)\rightarrow \Box A


Pravila izvoda su modus ponens: A, A\rightarrow B/B i pravilo nužnosti: A/\Box A. Na standardni način se definira pojam dokaza i teorema u sistemu GL. Ako je modalna formula A teorem sistema GL tada to označavamo s \textsf{GL}\vdash A.

Sada ćemo reći nešto o aritmetičkoj interpretaciji logike dokazivosti GL. Upravo aritmetička interpretacija daje pravo svjetlo na razloge zašto se razmatra logika dokazivosti. Aritmetička interpretacija sistema GL je svaka funkcija \ast sa skupa svih modalnih formula u skup svih rečenica teorije PA tako da za sve modalne formule A i B vrijedi:

\begin{array}{rcl} (P)^{\ast} & = & \text{proizvoljna aritmetička rečenica, gdje je }P\text{ propozicionalna varijabla}\\ (\neg A)^{\ast} & = & \neg A^{\ast}\\ (A\rightarrow B)^{\ast} & = & A^{\ast} \rightarrow B^{\ast}\\ (\Box A)^{\ast} & = & Pr (\lceil A^{\ast} \rceil) \end{array}

Sljedeći teorem govori da je modalnom logikom GL potpuno opisan predikat dokazivosti Pr teorije PA. Dokaz teorema možete pogledati u [3] i [12].



Solovajev teorem potpunosti, 1976.
Za svaku modalnu formuluA vrijedi}:
GL \vdash A ako i samo ako za svaku aritmetičku interpretaciju \ast imamo  PA \vdash A^{\ast}.


Neki veliki otvoreni problemi u ovom području su, primjerice, određivanje logike dokazivosti Heytingove aritmetike te određivanje logike dokazivosti nekih važnih fragmenata teorije PA.

Treba posebno naglasiti da više teorija ima istu logiku dokazivosti. Primjerice, logika dokazivosti Peanove aritmetike, Zermelo–Fraenkelove teorije skupova i Goedel–Bernaysove teorije skupova je modalni sistem GL. Prirodno se postavilo pitanje koja aritmetička svojstva teorija treba još razmatrati kako bi modalni opis predikata dokazivosti različitih teorija bili različiti. Jedan odgovor su logike interpretabilnosti. Moramo naglasiti da je glavni razlog spominjanja logika interpretabilnosti u ovom članku to što se one već više od 30 godina proučavaju u Zagrebu.

Proučavanje logika interpretabilnosti započelo je krajem osamdesetih godina prošlog stoljeća u Nizozemskoj (Utrecht i Amsterdam). Prvi radovi o tome prezentirani su na jednoj konferenciji 1990. godine. Iste godine Z. šikić je predavao kolegij o logici dokazivosti na doktorskom studiju matematike u Zagrebu (sadržaj kolegija je pratio knjigu [12]). Do današnjeg dana u Hrvatskoj su obranjena 4 doktorata s temama iz logika interpretabilnosti te su hrvatski matematičari autori znanstvenih članaka o logikama interpretabilnosti koji su objavljeni u vodećim logičkim časopisima kao što su: The Journal of Symbolic Logic, Annals of Pure and Applied Logic, Logic Journal of IGPL, Archive for Mathematical Logic, Studia Logica i Mathematical Logic Quarterly. Jako dobri prikazi logika interpetabilnosti dani su u [5] i [16].


Bibliografija
[1] J. Avigad, The mechanization of mathematics, Notices of the AMS, 65(6), 681–690, 2018.
https://www.ams.org/journals/notices/201806/rnoti-p681.pdf
 
[2] P. Blackburn, M. de Rijke, Y. Venema, Modal Logic, Cambridge University Press, 2001.
 
[3] G. Boolos, The Logic of Provability, Cambridge University Press, 1996.
 
[4] Y. Cheng, Current Research on Goedel's Incompleteness Theorems, Bulletin of Symbolic Logic 27 (2021), 113–167
 
[5] G. Japaridze, D. de Jongh, The Provability logic, u S. Buss (ur.), Handbook of Proof Theory, Elsevier, 1998, 475–546
 
[6] J. Kovačić, Nedokazive formule u Peanovoj aritmetici, diplomski rad, PMF–MO, Zagreb, 2011.
https://www.pmf.unizg.hr/_ownload/repository/Kovacic-Nedokazive-formule-...
 
[7] E. Nagel, J. R. Newman, Goedelov dokaz, Kruzak, Zagreb, 2001.
 
[8] T. Novak, Goedelovi teoremi nepotpunosti, diplomski rad, FER, Zagreb, 2011.
https://www.pmf.unizg.hr/_download/repository/Novak-Goedelovi-teoremi-ne...
 
[9] T. Perkov, M. Vuković, Semantike logika dokazivosti i interpretabilnosti, predavanja poslijediplomskog kolegija, PMF–MO, Zagreb, 2017.
https://www.pmf.unizg.hr/_download/repository/Semantike-logika-dokazivos...
 
[10] T. Perkov, M. Vuković, Algebarska semantika modalne logike, predavanja poslijediplomskog kolegija, PMF–MO, Zagreb, 2020.
https://www.pmf.unizg.hr/_download/repository/Algebarska-semantika-modalne-logike-2020\% 5B1\% 5D.pdf
 
[11] P. Smith, An Introduction to Goedel’s Theorems, Cambridge University Press, 2007.
 
[12] C. Smorynski, Self–reference and modal logic, Springer–Verlag, 1985.
 
[13] Z. šikić, život i djelo Kurta Goedela, Matematika, stručno-metodički časopis, 1987, br. 2, 49–59
 
[14] Z. šikić, Goedelovi teoremi, Rugjer 5 (1996), 30–35
https://www.fsb.unizg.hr/matematika/sikic/download/ZS_goedelovi\underline{\text{}\hskip 0.5em\text{}}teoremi.pdf
 
[15] Z. šikić, Goedelovi teoremi, Poučak 49 (2012), 16–30
https://hrcak.srce.hr/103874
 
[16] A.  Visser, An overview of interpretability logic, u K. Marcus et al. (ur.), Advances in modal logic. Vol. 1. Selected papers from the 1st international workshop (AiML'96), Berlin, Germany, October 1996, Stanford, CA: CSLI Publications, CSLI Lecture Notes 87(1998), 307–359
 
[17] M. Vuković, Goedelovi teoremi nepotpunosti, MFL 206 (2002), 74–79
https://www.pmf.unizg.hr/_download/repository/2001-MFL-Goedel.pdf
 
[18]

M. Vuković, Matematička indukcija i Goodsteinov teorem, Poučak 13 (2003), 5–13


https://www.pmf.unizg.hr/_download/repository/2003-Poucak-Goodstein.pdf
 

[19] M. Vuković, Matematička logika, Element, Zagreb, 2009.
 
[20] M. Vuković, Primijenjena logika, predavanja poslijediplomskog kolegija, PMF–MO, Zagreb, 2011.
https://www.pmf.unizg.hr/_download/repository/APPLOG-skripta-2011.pdf
 
[21] M. Vuković, Teorija skupova, predavanja, PMF–MO, Zagreb, 2015.
https://www.pmf.unizg.hr/_download/repository/TS-predavanja-2015.pdf



 
2Modalne logike su proširenja klasičnih logika s modalnim operatorima. Osnovna modalna logika je proširenje klasične logike sudova s modalnim operatorom \Box. Osnovne informacije o modalnoj logici možete pronaći u [19], dok u [2] postoji mnoštvo detalja o raznim modalnim logikama. Na doktorskom studiju matematike u Zagrebu održano je nekoliko kolegija gdje su se razmatrale modalne logike. Za neke od njih na internetu su dostupni nastavni materijali. U popisu literature ovog članka to su reference [9] i [10].

Topološka semantika logika dokazivosti

 

 

Luka Mikec i Tin Perkov

 

Sažetak
Modalna logika obuhvaća široku familiju formalnih jezika i sistema s brojnim primjenama u računarstvu, lingvistici, filozofiji, teoriji informacija itd. Modalna logika ima iznenađujuće jednostavnu sintaksu i relacijsku semantiku koja se gotovo bez modifikacija uklapa u prividno vrlo različite primjene. U ovom članku1 fokusiramo se na primjenu modalne logike koja je od možda najvećeg interesa za matematičare: formalizaciju Gödelovog2 predikata dokazivosti, ključnog pojma Gödelovih teorema nepotpunosti. Uobičajenim matematičkim postupkom apstrakcije, ključna svojstava predikata dokazivosti proglašena su aksiomima i polazeći od njih izgrađen je logički sistem. Uz standardnu relacijsku semantiku, topološka semantika također se pokazuje pogodnom, pa i nužnom za jedno proširenje logike dokazivosti koje razmatramo na kraju članka.

1Modalna logika


1.1Sintaksa i intendirana interpretacija

Modalna logika motivirana je potrebom da se formalizira nužnost i mogućnost, znanje i vjerovanje, dokazivost i mnoga druga svojstva koja se mogu smatrati operatorima na logičkim sudovima.3 Stroga izgradnja logičkog sustava, pa tako i modalne logike, podrazumijeva definiranje sintakse (jezik, izvod, dokaz, teorem) i semantike (model, istinitost, valjanost), te dokazivanje teorema adekvatnosti i potpunosti kao veze sintakse i semantike. U nastavku pretpostavljamo da su ovi pojmovi poznati iz logike sudova i logike prvog reda. Detalji se po potrebi mogu pronaći u svakom početnom udžbeniku matematičke logike, npr. [12].

U ovom članku razmatramo samo propozicionalne modalne logike. Najprije ćemo definirati alfabet osnovne modalne logike.

Alfabet osnovne modalne logike je proširenje alfabeta logike sudova simbolom \Box, tj. skup simbola koji sadrži:

\bullet prebrojivo mnogo propozicionalnih varijabli, koje označavamo p,q i sl.
\bullet logičke veznike \neg,\wedge,\vee,\to,\leftrightarrow
\bullet logičke konstante \top,\bot
\bullet \Box, koji zovemo modalni operator.


Formule modalne logike definiraju se rekurzivno:

\bullet propozicionalne varijable i logičke konstante su formule
\bullet ako su A i B formule, onda su \neg A, A\wedge B, A\vee B, A\to B, A\leftrightarrow B, \Box A također formule.


Definiramo dualni modalni operator \Diamond A kao pokratu za \neg\Box\neg A.

Napomena 1. Formulu oblika \Box A čitamo “nužno je A”, “agent4 zna A”, “dokazivo je A” i slično, ovisno o interpretaciji. Postavlja se pitanje za koje formule očekujemo da uvijek vrijede. Npr. ako formulu \Box A\to A čitamo kao “ako agent zna A, onda vrijedi A”, složit ćemo se da je to u skladu sa značenjem glagola “znati” u prirodnom jeziku. No, to nije slučaj ako \Box interpretiramo kao vjerovanje. Čitatelj može razmisliti i o sljedećim primjerima:
\bullet \Box A\to\Box\Box A
\bullet \Diamond A\to\Box\Diamond A
\bullet \Box(A\to B)\to(\Box A\to\Box B)
Formulu oblika \Diamond A često čitamo kao “ moguće je A” (“ nije nužno \neg A”).

Napomena 2. Očigledni pravci generalizacije modalne logike su jezici s više modalnih operatora (npr. za modeliranje sistema s više agenata; još jedan primjer je u posljednjoj točki ovog članka), kao i višemjesni modalni operatori (npr. za modeliranje algoritamskih koncepata kao što je relacija “until”: formulu oblika U(A,B), gdje je U dvomjesni modalni operator, čitamo kao “vrijedit će A sve do trenutka u kojem će početi vrijediti B”). Također, mogu se promatrati i modalne logike s kvantifikatorima, no u ovom članku razmatramo samo propozicionalne modalne sisteme.


Formula oblika \Box(A\to B)\to(\Box A\to\Box B), posljednja navedena u napomeni 1, u skladu je s gotovo svim interpretacijama operatora \Box koje se pojavljuju u primjenama, te se stoga uzima kao aksiom osnovnog modalnog sistema, kojeg zovemo sistem K (oznaka je u čast Kripkea5).

Definicija 3. Aksiomi sistema K su sve tautologije logike sudova, ali u proširenom jeziku (npr. \Box A \vee \neg\Box A je tautologija u modalnom jeziku), te svaka formula oblika
\Box(A\to B)\to(\Box A\to\Box B).
Pravila izvoda su modus ponens \displaystyle{\frac{A\quad A\to B}{B}} i generalizacija \displaystyle{\frac{A}{\Box A}}. Kažemo da je formula A teorem sistema K (oznaka: \vdash A) ako je A element najmanjeg skupa formula koji sadrži sve aksiome i zatvoren je na pravila izvoda.


Ovisno o intendiranoj interpretaciji, različiti modalni sistemi dobivaju se dodavanjem jednog ili više drugih aksioma, npr. formula \Box A\to A iz napomene 1. je jedan od aksioma epistemičke logike (u kojoj je \Box interpretiran kao operator znanja).

1.2Relacijska semantika

Za modalnu logiku postoji više vrsta semantike (relacijska, topološka, okolinska, algebarska, ... ). U ovom dijelu članka razmatramo relacijsku semantiku, koja se često naziva i Kripkeova semantika ili semantika mogućih svjetova. Kasnije ćemo upoznati i topološku semantiku.

Definicija 4. Kripkeov okvir (ili samo okvir) je uređeni par (W,R), gdje je W\neq\emptyset skup koji zovemo nosač, a R binarna relacija na W koju zovemo relacija dostiživosti. Elemente nosača zovemo svjetovi ili točke.

(Kripkeov) model je uređena trojka (W,R,V), gdje je (W,R) okvir, a V valuacija, funkcija koja svakoj propozicionalnoj varijabli p pridružuje podskup nosača V(p)\subseteq W.

Pritom kažemo da je formula p istinita u svijetu w\in W i pišemo w\Vdash p ako je w\in V(p). Definicija istinitosti rekurzivno se proširuje na sve formule:
\bullet za svaki svijet w vrijedi w\Vdash\top i w\not\Vdash\bot
\bullet w\Vdash\neg A ako ne vrijedi w\Vdash A
\bullet w\Vdash A\wedge B ako w\Vdash A i w\Vdash B
\bullet w\Vdash\Box A ako za svaki v\in W takav da je wRv vrijedi v\Vdash A.
Kažemo da je formula valjana na okviru (W,R) ako je istinita u svakom svijetu za svaku valuaciju na tom okviru. Pišemo \Vdash A ako je formula A valjana na svakom okviru.


Uočimo da iz definicije slijedi da je w\Vdash\Diamond A ako i samo ako postoji v\in W takav da je wRv i v\Vdash A.

Kripkeove modele možemo zamišljati kao jednostavne usmjerene grafove ako svakoj točki grafa (svijetu modela) x pridružimo neki skup propozicionalnih varijabli p za koje vrijedi x \in V(p).

Primjer 5. Na slici je jedan Kripkeov model. Skup svjetova W je skup \lbrace 0, 1, 2, 3, 4\rbrace. Vrijedi xRy ako i samo postoji strelica iz svijeta x u svijet y. Za svijet x \in W i propozicionalnu varijablu \ell vrijedi x \in V(\ell) ako i samo ako je \ell napisan pokraj x.


Pogledajmo nekoliko primjera istinitih i neistinitih formula u svijetu 0. Vrijedi li 0 \Vdash \Box p? Da, jer su iz svijeta 0 dostižni samo svjetovi 1 i 2, te u oba vrijedi p. U svijetu 1 nije istinito r, a u svijetu 2 nije istinito q. Stoga ne vrijedi 0 \Vdash \Box r niti 0 \Vdash \Box q. No, primijetimo da vrijedi 0 \Vdash \Diamond q te 0 \Vdash \Diamond r.

Ne vrijedi 0 \Vdash \Diamond s (postoji put, ali ne postoji strelica, iz 0 u 3). Ali, vrijedi 0 \Vdash \Diamond \Diamond s. Zatim, iako ne vrijedi 0 \Vdash \Box q, vrijedi 0 \Vdash \Box (q \vee \Diamond q).

Još neki primjeri formula koje su istinite u 0 su \Box(r \to \Diamond\Diamond\Box s), \Diamond\Diamond\Diamond\Diamond s i \Box(\Diamond q \to \Diamond s). Primijetite petlju na slici. Ona je bitna za istinitost prvih dviju navedenih formula.

Neke formule koje nisu istinite u svijetu 0 su primjerice sljedeće: \Box(\Box q \to q) \to \Box q, \neg q \to \Box \Diamond \neg q i \Diamond \Diamond s \to \Diamond s.


Na internetu postoje stranice na kojima je moguće konstruirati primjere Kripkeovih modela i ispitivati istinitost formula. Jedna takva stranica je na adresi http://rkirsling.github.io/modallogic/.

Sada smo modalnim formulama dali matematičko značenje, pa možemo o ranije spomenutim primjerima formula razmišljati na precizniji način.

Primjer 6. Svaka formula oblika \Box A\to A je valjana na okviru (W,R) ako i samo ako je R refleksivna relacija.

Zaista, neka je R refleksivna i w\in W takav da je w\Vdash\Box A. To znači v\Vdash A za sve v takve da je wRv. No zbog refleksivnosti relacije R vrijedi wRw, pa je posebno w\Vdash A. Iz w\Vdash\Box A zaključili smo w\Vdash A, što po semantici logičkog veznika \to povlači w\Vdash\Box A\to A.

Obratno, neka je svaka formula oblika \Box A\to A valjana na okviru (W,R). Pretpostavimo da R nije refleksivna, tj. postoji w\in W takav da ne vrijedi wRw. Neka je V valuacija takva da je V(p)=W\setminus\lbrace w\rbrace. Lako se vidi da tada vrijedi w\Vdash\Box p, ali ne w\Vdash p, dakle u w nije istinita \Box p\to p, što je u kontradikciji s pretpostavkom.


Iz prethodnog primjera slijedi da okviri za epistemičku logiku, u kojoj su formule oblika \Box A\to A aksiomi, nužno imaju refleksivnu relaciju dostiživosti.

Zadatak 7. Neka je (W,R) okvir. Slično kao u prethodnom primjeru, dokažite:
\bullet \Box A\to \Box\Box A je valjana na (W,R) ako i samo ako je R tranzitivna
\bullet \Diamond A\to\Box\Diamond A je valjana na (W,R) ako i samo ako R ima sljedeće svojstvo: za sve w,v,u\in W, ako je wRv i wRu, onda je vRu
\bullet \Box(A\to B)\to(\Box A\to\Box B) je valjana na svakom okviru.


Općenito, nužni i dovoljni uvjeti da se neko svojstvo relacije može definirati modalnom formulom dani su poznatim Goldblatt–Thomasonovim teoremom (detalji se mogu vidjeti npr. u knjizi [2]).

Za sistem K vrijedi teorem adekvatnosti i potpunosti u odnosu na relacijsku semantiku, tj. za svaku formulu A vrijedi: \vdash A ako i samo ako \Vdash A. Adekvatnost slijedi iz prethodnog zadatka, dok dokaz potpunosti nadilazi okvire ovog članka. Spomenimo, također bez dokaza, da za modalni sistem dobiven dodavanjem aksioma \Box A\to A sistemu K vrijedi adekvatnost i potpunost u odnosu na klasu svih okvira čija je relacija dostižnosti refleksivna. Analogni rezultati vrijede i za ostale spomenute formule, ali i mnoge druge (v. npr. [6]).

2Logika dokazivosti – sistem GL

2.1Sintaksa i aritmetička interpretacija

Sistem GL (Gödel, Löb6) proširenje je osnovnog modalnog sistema K svim formulama oblika \Box(\Box A \to A) \to \Box A kao aksiomima. Shema formula \Box(\Box A \to A) \to \Box A naziva se Löbovim aksiomom i označava s L. Uvodimo oznaku \vdash_{GL}A za modalnu formulu A koja je teorem sistema GL.

Sada ćemo reći nešto o tome što predstavljaju teoremi sistema GL. Radi se o određenoj vezi s Peanovom aritmetikom i drugim formalnim teorijama aritmetike. Peanova aritmetika je jedna teorija prvog reda (v. [12]).

Pišemo \vdash_{PA}A ako je A teorem Peanove aritmetike. Predikat dokazivosti Peanove aritmetike je formula Pr(n) čije je neformalno značenje “broj n je kod nekog teorema Peanove aritmetike”.

Prostor nam ne dopušta da pobliže obrazložimo postupak kodiranja koji omogućuje da se dokazivost formula Peanove aritmetike izrazi u samoj Peanovoj aritmetici. Detalji ove konstrukcije mogu se vidjeti u knjizi [9], ili u sažetoj skripti te knjige namijenjenoj studentima7.

Jednom kad smo konstruirali predikat dokazivosti ili se već nekako uvjerili da on postoji, prirodno je pitati se koja su njegova svojstva. Ako je A neka formula Peanove aritmetike, s \ulcorner A \urcorner ćemo označavati njezin kod.

Podsjetimo da je rečenica bilo koja zatvorena formula prvog reda, tj. formula čije su sve varijable u dosegu kvantifikatora. Jedno prirodno pitanje koje bi nas moglo zanimati jest je li formula Pr(\ulcorner A \urcorner) \to A (“ako je A dokaziva, onda vrijedi A”) teorem aritmetike za svaku rečenicu A. Poznati Löbov teorem za Peanovu aritmetiku kaže da je za danu rečenicu A, formula Pr(\ulcorner A \urcorner) \to A dokaziva jedino ako je već i sama formula A dokaziva. Uočimo da to zapravo govori o slabosti Peanove aritmetike. Löbov teorem je tvrdnja koja govori o Peanovoj aritmetici. No, dokaz tvrdnje tog teorema moguće je provesti i unutar same Peanove aritmetike. Pritom je tvrdnja Löbovog teorema formalizirana sljedećom formulom:

Pr(\ulcorner Pr(\ulcorner A \urcorner) \to A\urcorner) \to Pr(\ulcorner A \urcorner).

Primijetimo da je ova formula sintaktički nalik shemi aksioma L sistema GL.

Sada ćemo precizirati vezu logike dokazivosti i aritmetike.

Definicija 8. Aritmetička interpretacija sistema GL je svaka funkcija * sa skupa svih modalnih formula u skup rečenica Peanove aritmetike sa sljedećim svojstvima:
\bullet svakoj propozicionalnoj varijabli p pridružena je proizvoljna rečenica p^{*};
\bullet funkcija ^{*} komutira s logičkim veznicima (npr. (A \wedge B)^{*} = A^{*} \wedge B^{*});
\bullet za svaku modalnu formulu A vrijedi (\Box A)^{*} = Pr(\ulcorner A^{*} \urcorner).


Solovayev8 prvi teorem govori o aritmetičkoj potpunosti sistema GL.

Teorem 9.[Solovay, 1976] Neka je A proizvoljna modalna formula. Tada vrijedi \vdash_{GL}A ako i samo ako je \vdash_{PA}A^{*} za sve aritmetičke interpretacije ^{*}.


Solovayev teorem nam govori da je, u određenom smislu, sve što Peanova aritmetika može reći o predikatu dokazivosti sadržano u teoriji \textbf{GL}. Vidimo da je njezin aksiom L upravo formalizacija Löbovog teorema. Izrečena veza je vrijedan rezultat jer Peanova aritmetika ima svojstvo neodlučivosti. Neodlučivost teorije je svojstvo da ne postoji algoritam koji će za danu formulu u konačno mnogo koraka ispravno reći je li ona teorem. S druge strane, \textbf{GL} je odlučiva teorija. U idućem ćemo poglavlju napomenuti kako bi izgledao algoritam koji određuje je li dana formula teorem sistema \textbf{GL}. Dakle, kroz sistem \textbf{GL} možemo na jednostavan način, štoviše potpuno mehanički, odgovoriti na preostala pitanja poput ranijeg (negativno odgovorenog) “je li Pr(\ulcorner A \urcorner) \to A teorem aritmetike za svaku rečenicu A?”

2.2Relacijska semantika

Ranije smo spomenuli da za sistem K proširen novom shemom aksioma \Box A \to A vrijede teoremi adekvatnosti i potpunosti u odnosu na klasu svih okvira kod kojih je relacija dostiživosti refleksivna. Sličan rezultat vrijedi za sistem GL.

Zadatak 10. Neka je (W,R) okvir. Kažemo da je relacija R inverzno dobro fundirana ako ne postoji niz svjetova (w_{i})_{i \in \mathbb{N}} takav da vrijedi w_{0} R w_{1} R w_{2}\dots

Dokažite: ako je R tranzitivna i inverzno dobro fundirana, onda je Löbov aksiom valjan na (W,R).


Napominjemo da vrijedi i obrat, koji je nešto teže dokazati, no zainteresiraniji čitatelj može pokušati. No, već i lakši smjer dovoljan je za ključni dio dokaza teorema adekvatnosti za sistem GL, tj. da za svaki formulu A vrijedi: ako je \vdash_{GL}A, onda je A valjana na svakom tranzitivnom i inverzno dobro fundiranom okviru. Vrijedi i obrat, tj. teorem potpunosti, čiji dokaz je, kao što je to i obično slučaj u logici, bitno složeniji. Može se pronaći npr. u knjigama [3] i [10].

Primijetimo da su konačna (tranzitivna) stabla poseban slučaj tranzitivnih inverzno dobro fundiranih relacijskih struktura. Stoga je klasa konačnih tranzitivnih stabala adekvatna za GL. No, vrijedi i potpunost.

Teorem 11. Neka je A proizvoljna modalna formula koja nije teorem sistema GL. Tada postoji konačno stablo (W, R), valuacija V i svijet w \in W tako da vrijedi w \nVdash A.

Ovo je vrlo značajan teorem. Prvo, on se na esencijalan način koristi u Solovayevu teoremu aritmetičke potpunosti. Drugo, on nam daje algoritam provjere je li neka formula A teorem sistema GL. Naprosto simultano prolazimo svim dokazima teorema sustava GL (npr. leksikografski od kraćih ka duljima), i svim konačnim stablima i njihovim valuacijama. Prije ili kasnije će se dogoditi nešto od sljedećeg:

\bullet pronaći ćemo dokaz formule A;
\bullet pronaći ćemo model u čijem je nekom svijetu istinita formula A.



2.3Topološka semantika

Sada želimo izgraditi još jednu semantiku za sistem GL. Ovoga puta kao temeljnu strukturu ne želimo koristiti okvire već topološke prostore. Naime, u posljednjem dijelu članka promatrat ćemo sistem u kojem nije moguće (na zadovoljavajuć način) definirati relacijsku semantiku, pa moramo posegnuti za topološkom. No, prije toga će nam sistem GL poslužiti kao jednostavniji primjer na kojem ćemo upoznati taj tip semantike. U nastavku pretpostavljamo poznavanje osnovnih pojmova topologije, kao što su topološki prostor, baza, uređajna topologija, gomilište, diskretna topologija i sl. Ako je čitatelju potreban podsjetnik, sve potrebne definicije mogu se pronaći npr. u [11].

Neka je (X,\mathcal{T}) topološki prostor. Na njemu možemo definirati model na posve analogan način kao i na okviru. Ono što trebamo promijeniti je definicija istinitosti za formule oblika \Box A. Naime, u topološkom prostoru više nemamo relaciju dostižnosti.

Definicija 12. Topološki model je uređena trojka (X,\mathcal{T},V), gdje je (X,\mathcal{T}) topološki prostor, a V valuacija, funkcija koja svakoj propozicionalnoj varijabli p pridružuje V(p)\subseteq X.

Istinitost modalnih formula u točki x\in X definira se rekurzivno, pri čemu su slučajevi propozicionalnih varijabli, logičkih konstanti i formula dobivenih primjenom logičkih veznika isti kao kod relacijske semantike, te se definira x\Vdash\Box A ako postoji U\in\mathcal{T} takav da je x\in U i za sve y\in U takve da je y\neq x vrijedi y\Vdash A.

Kažemo da je formula valjana na topološkom prostoru (X,\mathcal{T}) ako je istinita u svakoj točki svakog topološkog modela (X,\mathcal{T}, V).


Uočimo da je x\Vdash\Diamond A ako i samo ako za svaki U\in\mathcal{T} takav da je x\in U postoji y\in U takav da je y\neq x i y\Vdash A. Drugim riječima, x\Vdash\Diamond A ekvivalentno je s činjenicom da je x gomilište skupa \lbrace y\in X:y\Vdash A\rbrace.

Kažemo da je topološki prostor (X,\mathcal{T}) raspršen ako svaki neprazan podskup S\subseteq X ima izoliranu točku, tj. postoji točka s \in S i neka njena okolina O\in\mathcal{T} tako da vrijedi S \cap O = \lbrace s \rbrace.

Primjer 13. Trivijalni primjer raspršenog prostora je diskretni topološki prostor. Netrivijalni primjer je (\alpha,\mathcal{T}), gdje je \alpha ordinal, a \mathcal{T} uređajna topologija. Naime, svaki S\subseteq\alpha je dobro uređen, pa ima najmanji element \min S. On je izolirana točka, jer \left[0,\min S+1\right\gt \in\mathcal{T} siječe S samo u \min S.

Propozicija 14. Formula \Box(\Box A\to A)\to\Box A je valjana na topološkom prostoru (X,\mathcal{T}) ako i samo ako je on raspršen.

Propozicija se dokazuje raspisivanjem definicija, na sličan način kao 6.

Adekvatnost i potpunost sistema GL u odnosu na klasu svih raspršenih topoloških prostora dokazao je Esakia9 1981. Iako je sam teorem dobro poznat, njegov dokaz je, koliko nam je poznato, objavljen samo u publikaciji [4] i nije nam dostupan. Međutim, za pretpostaviti je da je Esakijin dokaz sličan ovdje navedenom.

Uvedimo jednu oznaku. Neka je dan okvir (X, R). Za točku x \in X označimo s R[x] skup \lbrace y \in X \ | \ xRy \rbrace.

Propozicija 15. Neka je R tranzitivna i inverzno dobro fundirana relacija na skupu X. Označimo B = \lbrace R[x] \cup \lbrace x\rbrace \ | \ x \in X \rbrace. Tada je familija B baza za neku topologiju \mathcal{T}. Štoviše, (X, \mathcal{T}) je raspršen prostor.

Prethodna propozicija ima jednostavan dokaz (v. [8]).

U dokazu idućeg teorema ćemo s \Vdash_{R} označavati istinitost u Kripkeovom modelu, a s \Vdash_{T} istinitost u topološkom modelu.

Teorem 16.[topološka potpunost] Neka je F formula koja je valjana na svim raspršenim topološkim prostorima. Tada vrijedi \vdash_{GL}F.

Dokaz. Neka vrijedi \nvdash_{\textbf{}}{GL} F. Tada (zbog potpunosti u odnosu na relacijsku semantiku – vidjeti teorem 11) postoji model (W, R, V) takav da je R tranzitivna i inverzno dobro fundirana, te točka w \in W takva da vrijedi w \nVdash_{R} F.

Neka je topologija \mathcal{T} generirana familijom B sljedećeg oblika:
B = \lbrace \lbrace x\rbrace \cup R[x] \ | \ x \in W \rbrace .
Tada iz prethodne propozicije proizlazi da je prostor (W, \mathcal{T}) raspršen, a familija B čini bazu za \mathcal{T}.

Promotrimo topološki model (W, \mathcal{T},V) s istim nosačem i valuacijom kao (W,R,V). Dokažimo da za sve formule G i točke x \in W vrijedi:
x \Vdash_{R} G \text{ ako i samo ako } x \Vdash_{T} G.
Tvrdnju dokazujemo indukcijom po složenosti formule G. Jasno je da tvrdnja vrijedi za bazu, te korak indukcije za slučaj logičkih veznika. Promotrimo korak indukcije za slučaj G = \square H. Neka je x \in W proizvoljna točka.

Neka vrijedi x \Vdash_{R} G. Dakle, za sve točke y \in R[x] vrijedi y \Vdash_{R} H. Kako je H manje složenosti od G, po pretpostavci indukcije za sve točke y \in R[x] vrijedi y \Vdash_{T} H. Kratko pišemo R[x] \Vdash_{T} H. No iz definicije baze B slijedi da je \lbrace x\rbrace \cup R[x] okolina točke x, pa po definiciji istinitosti u točki topološkog modela slijedi x \Vdash_{T} G. Slično se dokazuje i obrat.

Sada iz ranije dokazane činjenice w\nVdash_{R} F i upravo dokazane tvrdnje slijedi w \nVdash_{T} F.
\ \blacksquare


Teoremi adekvatnosti i potpunosti za GL u odnosu na topološku semantiku ponekad se formuliraju tako da se kaže da je “GL logika raspršenih prostora”. Semantike modalnih logika nam olakšavaju analizu njihovih svojstava. Primjerice, puno je lakše semantički argumentirati da neka formula nije teorem dane modalne logike. No veza je dvosmjerna. Primjerice, dobro je poznato da su formule oblika \Diamond \Diamond A \to \Diamond A teoremi sustava GL. No iz činjenice da je “GL logika raspršenih prostora” odmah slijedi da je za svaki raspršen prostor (X, \mathcal{T}) i njegov podskup S \subseteq X, skup gomilišta skupa gomilišta od S podskup skupa gomilišta od S.

3Polimodalna logika dokazivosti – GLP

Vidjeli smo vezu između GL i raspršenih prostora. No, vidjeli smo i da za GL imamo jednostavnu relacijsku semantiku. Važnost se topološkog pristupa vidi tek u proširenjima sistema GL.

3.1Uvod

Sistem GLP uveo je Japaridze10 1986. Radi se o proširenju sistema GL s prebrojivo mnogo modalnih operatora [n] indeksiranih prirodnim brojevima.11 Formule sistema GLP se definiraju rekurzivno, slično kao formule sistema GL. Naglasimo samo dio definicije koji se odnosi na nove modalne operatore: ako je A formula, onda je i [n]A formula (za sve prirodne brojeve n). Slično kao ranije, koristimo pokratu {\left\lt n\right\gt }A za \neg[n]\neg A.

Aksiomi su sve tautologije (u novom jeziku!), te sheme aksioma:

\bullet (K_{n})[n](A\to B)\to([n]A\to[n]B)
\bullet (L_{n})[n]([n]A\to A)\to[n]A
\bullet (P_{n}^{m})[n]A\to[m]A, ako je n\lt m
\bullet (Q_{n}^{m}){\left\lt n\right\gt }A\to[m]{\left\lt n\right\gt }A, ako je n\lt m


Uočimo da prve dvije sheme aksioma sugeriraju da se radi o nizu operatora dokazivosti, dok druge dvije određuju odnos među njima. Pravila izvoda su modus ponens i \displaystyle{\frac{A}{[n]A}}, n\in\mathbb{N}.

Aritmetička interpretacija sistema GLP je svaka funkcija * sa skupa svih formula sistema GLP u skup rečenica Peanove aritmetike sa svojstvima analognim aritmetičkoj interpretaciji sistema GL, pri čemu je [0] interpretiran kao \Box, tj. ([0]A)^{*} = Pr(\ulcorner A^{*}\urcorner), te je ([n]A)^{*} definirana tako da, neformalno govoreći, ima značenje “A^{*} je dokaziva u teoriji proširenoj svim istinitim \Pi_{n} rečenicama”, gdje su \Pi_{n} rečenice one koje sadrže kvantifikatore samo na početku formule i imaju n alternacija kvantifikatora od kojih je prvi \forall. Potrebno je dokazati da je ovako definirani niz predikata dokazivosti moguće formalizirati koristeći kodiranje, no ovdje nećemo ulaziti u detalje.

Aritmetičku adekvatnost i potpunost dokazao je Japaridze u radu [5].

3.2Relacijska semantika?

Okvir za polimodalnu logiku je relacijska struktura s nosačem W\neq\emptyset i indeksiranom familijom relacija dostižnosti pridruženih modalnim operatorima. Istinitost formula definira se za svaki modalni operator analogno kao za \Box u slučaju osnovnog modalnog jezika. Dakle, u slučaju sistema GLP okvir bi bio (W,(R_{n})_{n\in\mathbb{N}}), R_{n}\subseteq W\times W, n\in\mathbb{N}, a iz definicije istinitosti istaknimo samo da se definira w\Vdash[n]A ako za sve u takve da je wR_{n}u vrijedi u\Vdash A.

Analogno sistemu GL, [n]([n]A\to A)\to[n]A je valjana ako i samo ako je R_{n} tranzitivna i inverzno dobro fundirana.

Zadatak 17. Dokažite da vrijedi:
\bullet [n]A\to[n+1]A je valjana na okviru (W,(R_{n})_{n\in\mathbb{N}}) ako i samo ako R_{n+1}\subseteq R_{n}
\bullet {\left\lt n\right\gt }A\to[n+1]{\left\lt n\right\gt }A je valjana na okviru (W,(R_{n})_{n\in\mathbb{N}}) ako i samo ako wR_{n}v i wR_{n+1}u povlači uR_{n}v.

Korolar 18. Ako su na okviru (W,(R_{n})_{n\in\mathbb{N}}) valjani svi aksiomi sistema GLP, onda je R_{n}=\emptyset za svaki n\gt 0.

Dokaz. Pretpostavimo R_{1}\neq\emptyset, tj. postoje w,u tako da je wR_{1}u. No, tada iz prve tvrdnje prethodnog zadatka slijedi wR_{0}u, a onda iz druge tvrdnje uR_{0}u, dakle imamo beskonačan niz uR_{0}uR_{0}u\dots, što je nemoguće jer je R_{0} inverzno dobro fundirana. Dakle, R_{1}=\emptyset, pa iz prve tvrdnje zadatka slijedi tvrdnja.
\ \blacksquare


Dakle, postoji samo trivijalna relacijska semantika za GLP. Stoga koristimo topološku semantiku.

3.3Topološka semantika

Neka je X\neq\emptyset i (X,\mathcal{T}_{n}) topološki prostor, za svaki n\in\mathbb{N}. Uređeni par (X,(\mathcal{T}_{n})_{n\in\mathbb{N}}) zvat ćemo politopološki prostor. Za S\subseteq X, s dS standardno se označava skup gomilišta skupa S. U politopološkom prostoru ćemo s d_{n}S označavati skup gomilišta skupa S s obzirom na topologiju \mathcal{T}_{n}.

Definicija 19. Politopološki model je uređena trojka (X,(\mathcal{T}_{n})_{n\in\mathbb{N}},V), gdje je (X,(\mathcal{T}_{n})_{n\in\mathbb{N}}) politopološki prostor i V valuacija. Istinitost formula definirana je analogno topološkoj semantici sistema GL. Istaknimo samo da se definira x\Vdash[n]A ako postoji U\in\mathcal{T}_{n} takav da je x\in U i za sve y\in U takve da je y\neq x vrijedi y\Vdash A.

Kažemo da je formula valjana na politopološkom prostoru (X,(\mathcal{T}_{n})_{n\in\mathbb{N}}) ako je istinita u svakoj točki svakog politopološkog modela (X,(\mathcal{T}_{n})_{n\in\mathbb{N}},V).


Uočimo da vrijedi x\Vdash{\left\lt n\right\gt }A ako i samo ako je x\in d_{n}\lbrace y\in X:y\Vdash A\rbrace.

Istaknimo teorem adekvatnosti topološke semantike za GLP.

Teorem 20. Neka je (X,(\mathcal{T}_{n})_{n\in\mathbb{N}}) politopološki prostor takav da za svaki n\in\mathbb{N} vrijedi:
(1) (X,\mathcal{T}_{n}) je raspršen topološki prostor
(2) \mathcal{T}_{n}\subseteq\mathcal{T}_{n+1} (tj. \mathcal{T}_{n+1} je finija topologija od \mathcal{T}_{n})
(3) za svaki S\subseteq X vrijedi d_{n}S\in\mathcal{T}_{n+1}
Tada je svaki teorem sistema GLP valjan na (X,(\mathcal{T}_{n})_{n\in\mathbb{N}}).

Dokaz ovog teorema prepuštamo čitatelju (detalji se mogu pronaći i u radu [8]).

Politopološke prostore za koje vrijede pretpostavke prethodnog teorema zovemo GLP-prostori. Potpunost sistema GLP u odnosu na GLP-prostore dokazana je u članku [1]. Detaljnije o dokazu potpunosti govori se i u [8].{00}

Bibliografija
[1] L. Beklemishev, D. Gabelaia: Topological completeness of provability logic GLP, Annals of Pure and Applied Logic 164 (2013) 1201–1223.
[2] P. Blackburn, M. de Rijke, Y. Venema: Modal Logic, Cambridge University Press, 2001.
[3] G. Boolos: The Logic of Provability, Cambridge University Press, 1995.
[4] L. Esakia: Dijagonalne konstrukcije, Löbova formula i Cantorovi raspršeni prostori, u: Istraživanja u logici i semantici, str. 128–-143, Metsniereba, Tbilisi 1981. (na ruskom jeziku)
[5] G. Japaridze: Polimodalna logika dokazivosti, u: Intenzionalne logike i logička sturktura teorija, str. 16–48, Metsniereba, Tbilisi 1988. (na ruskom jeziku)
[6] J. Garson: Modal logic, u: E. N. Zalta (ur.) The Stanford Encyclopedia of Philosophy, Stanford University, 2016. (pristupljeno 16. 2. 2017. na https://plato.stanford.edu/entries/logic-modal/)
[7] I. Gavran, M. Vuković: Logička analiza hibridnih sustava, Poučak 58 (2014) 4–16.
[8] L. Mikec: Topološka potpunost logika dokazivosti (diplomski rad), Prirodoslovno-matematički fakultet – Matematički odsjek, 2016. (pristupljeno 16. 2. 2017. na https://www.math.pmf.unizg.hr/sites/default/files/pictures/mikec-toplosk...)
[9] P. Smith: An Introduction to G"odel's Theorems, Cambridge University Press, 2007.
[10] C. Smorynski: Self–Reference and Modal Logic, Springer, 1985.
[11] Š. Ungar: Opća topologija (materijali za kolegij), Zagreb 2012. (pristupljeno 16. 2. 2017. na https://web.math.pmf.unizg.hr/~ungar/NASTAVA/OT/)
[12] M. Vuković: Matematička logika, Element, Zagreb 2009.
 


 

Broj 32

Dragi čitatelji,

 

objavljen je 32. broja časopisa math.e. U ovom broju donosimo članke na temu matematičkih nejednakosti, metodike nastave matematike (vizualni dokazi) i logike dokazivosti. U članku Beesackova nejednakost, autora Ivane Sočo i Maje Andrić dan je prikaz nekoliko različitih metoda dokaza Beesackove klase nejednakosti. Pored prikaza nekoliko bitno različitih pristupa dokazu ovij nejednakosti, što je od interesa studentima prvih kurseva iz matematičke analize, prezentirane su i zanimljive ilustracije metoda dokaza. U članku Vizualni i kratki dokazi - prilog kreativnoj nastavi matematike (1.dio), autora Darka Veljana i Ivane Marušić prikazujemo prvi u nizu članaka o vizualnim dokazima u matematici. Time na zanimljiv način nastavljamo ilustracijski niz iz prethodnog članka. Ovaj rad može biti posebno zanimljiv studentima nastavničkog smjera kao i nastavnicima u radu s darovitim učenicima. Topološka semantika logika dokazivosti, autora Luke Mikeca i Tina Perkova daje prikaz topološkog pristupa modalnoj logici. Time također imamo vizualan pristup važnim matematičkim konceptima, posebno u temeljnim računarskim znanostima.

U ime uredništva časopisa želim vam ugodno čitanje i uspješnu 2018.

 

Luka Grubišić