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.




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




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.






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





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








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




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.




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:





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





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