U ranijem tekstu zašto matematika ne može zahvatiti istinu? bilo je riječi o prvom Gödelovom (Gödel-Rosserovom) teoremu:
Uobičajene matematičke teorije, npr. uobičajene formalne aritmetike i teorije skupova, nisu formalno potpune (a čak niti upotpunjive), tj. za takve teorije mora postojati barem jedna rečenica izražena u jeziku te teorije takva da niti ona sama, niti njena negacija nisu dokazive u toj teoriji (nisu teoremi te teorije).
Kako svaka rečenica o primjerice prirodnim brojevima ipak ili jest ili nije istinita, a niti jedna se teorija aritmetike ne može odlučiti o baš svakoj rečenici, to znači da nikakvim formalnim teorijama niti u principu ne možemo (potpuno) zahvatiti sve istine o prirodnim brojevima.
To je bio prvi Gödelov teorem nepotpunosti, a ovdje je riječ o povijesti i relevantnosti drugog Gödelovog teorema nepotpunosti. Cilj ovog teksta zapravo je dati uvod i iznijeti gledišta iz nedavnog (preprinta) članka The Provability of Consistency (Sergei Artemov).
Kroz povijest su razmatrane neke teorije za koje se kasnije ispostavilo da su inkonzistentne, tj. u njima je moguće dokazati i R i ne-R za neku rečenicu R. Popularan primjer je Russellov paradoks. Može se pokazati da se u inkonzistentnim teorijama može dokazati bilo što (ex falso quodlibet), pa se ne možemo oslanjati na rezultate dokazane u inkonzistentnim teorijama. Kako je svojstvo inkonzistentnosti u uobičajeno razmatranim teorijama ekvivalentno s time da je npr. dokazivo 0 = 1 ili 2 + 2 = 5 ili druge slične tvrdnje, u nastavku ćemo uzeti da “teorija T je konzistentna” znači “teorija T ne dokazuje 0 = 1”.
Zbog ranije uočenih inkonzistentnih teorija, početkom dvadesetog stoljeća javila se ideja da bi bilo dobro matematički dokazati da su matematičke teorije (one koje su se tada koristile) konzistentne. Cilj je ovdje donekle filozofski određen: nije precizirano što bi značilo “dokazati konzistentnost matematičke teorije”, odnosno, nije odmah jasno kakvu bi to matematičku tvrdnju trebalo dokazati a da se na temelju takvog preciznog matematičkog dokaza može reći “dokazali smo konzistentnost jedne matematičke teorije.” Primjerice, nije posebno kontroverzno što znači da su “matematičari dokazali da ne postoji najveći prost broj.” Tvrdnju da ne postoji najveći prost broj vrlo lako možemo izraziti kao svojstvo uobičajenih matematičkih objekata (brojeva, skupova itd.), i aksiomi koji su nam potrebni za dokaz takve tvrdnje vrlo su dobro prihvaćeni. Stoga nije posebno kontroverzno jesu li matematičari dokazali da ne postoji najveći prost broj. No, “dokazati konzistentnost matematičke teorije” nema neku očitu precizaciju i formalizaciju. (Štoviše, osim što nije bilo jasno kakva bi se precizna, formalna i matematička tvrdnja trebala dokazati, nije bilo jasno niti koliko se snažni aksiomi i pravila zaključivanja smiju koristiti a da nam dokaz bude prihvatljiv.)
Dva su velika i poznata matematička rezultata koji govore nešto o dokazivosti konzistentnosti matematičkih teorija: Gödelov i Gentzenov (na dnu ovog teksta je kratka napomena o Gentzenovom). Prvi od njih, Gödelov, koji je vjerojatno i prihvaćeniji kao relevantniji za projekt (pokušavanja) dokazivanja konzistentnosti, poznat je kao drugi Gödelov teorem nepotpunosti. On se obično izražava na sljedeći način:
Uobičajene matematičke teorije ne mogu za sebe dokazati da su konzistentne.
Gödelov drugi teorem potpunosti
Uobičajeno je izreći Gödelov drugi teorem kao iznad, u terminima iz kojih se čini da on daje direktan odgovor na ranije postavljeno pitanje o tome možemo li dokazati konzistentnost matematičkih teorija (recimo, dokazati unutar teorija koje nisu jače od njih samih). No, iz takve verzije ne doznajemo ništa o tome što je zapravo dokazano. Stoga je ovdje u nastavku prvo okvirno “otpakiravanje” te tvrdnje do nešto preciznijih tvrdnji, dok ne postane malo jasnije što taj teorem tvrdi.
Za svaku uobičajenu teoriju T postoji tvrdnja, označimo ju s Con(T), koja formalizira sljedeću tvrdnju:
T je konzistentna.
Gödelov teorem kaže da ako je Con(T) teorem neke uobičajene teorije T, onda je T inkonzistentna. Kako su uobičajene teorije adekvatne (“istinite”, sound), slijedi da Con(T) ne može biti dokaziva tvrdnja. No Con(T) smo izrazili koristeći nejasan termin “konzistentno”. Kako to napisati kao uobičajenu matematičku tvrdnju poput “za svaki x postoji y takav da je x + 5 = y – 2”?
Ne postoji dokaz d u teoriji T toga da 0 = 1.
Ako Con(T) zapišemo ovako, više nemamo (mutne) termine poput “dokazivo” i “konzistentno”, ali i dalje nemamo tvrdnju koja govori o brojevima. Jezikom aritmetike možemo izraziti da “nešto postoji”, ali ne (barem ne direktno) da je to nešto “dokaz” – intendirana interpretacija aritmetike je skup prirodnih brojeva, ne skup dokaza. Taj se problem može riješiti trikom aritmetizacije, odnosno kodiranjem.
Ne postoji broj d koji kodira dokaz u teoriji T toga da 0 = 1.
Objekti nalik brojevima
Može se dokazati (zanimljivim i ne pretjerano teškim, ali dugim dokazom) da se gornja rečenica doista može zapisati kao aritmetička rečenica (koristeći samo kvantifikatore “za svaki”, “za neki”, te simbole 0, 1, +, * i =). Za daljnji tekst je već ovako napisana formalizacija (gotovo) dovoljno precizna. Artemov misli da su već do ove točke otpakiravanja iskaza Gödelovog drugog teorema nepotpunosti napravljeni koraci koji se mogu smatrati upitnima u odnosu na vezu sa značenjem početnog pitanja (dokazivost konzistentnosti). Potreban je još jedan (mali ali bitan) korak. Prirodni brojevi jesu intendirana interpretacija aritmetičkih teorija, ali te su teorije zapravo o bilo kakvim objektima koji se ponašaju dovoljno slično brojevima. Odnosno, aritmetičke teorije nisu samo o stvarno postojećim prirodnim brojevima. Sličnost s brojevima prisutna je u mjeri u kojoj tu sličnost uspijemo ugraditi u aksiome; nažalost, razni fundamentalni teoremi u matematičkoj logici pokazuju da razumnim aksiomima ne možemo u potpunosti zahvatiti ponašanje prirodnih brojeva. Stoga, ne možemo baš formalizirati “postoji broj” iz posljednje formulacije Con(T), ali možemo formalizirati “postoji objekt nalik broju“: ta će formalizacija, jer aritmetičke teorije već jesu (samo) o “objektima nalik brojevima”, biti običan kvantifikator “postoji”. O ovom problemu brojeva i objekata nalik brojeva bit će malo više riječi ispod. Za objekte nalik brojevima znamo da imamo zbrajanje, množenje, indukciju kao alate koji se ponašaju vrlo slično verzijama tih koncepata za prirodne brojeve, i općenito znamo da ti objekti ispunjavaju brojna svojstva stvarnih prirodnih brojeva.
Ne postoji d koji kodira dokaz u teoriji T toga da 0 = 1.
Ekvivalentno:
Za svaki d vrijedi: d ne kodira dokaz u teoriji T toga da 0 = 1.
Iz ove će formulacije Con(T) biti jasno gdje Artemov vidi problem s uobičajenom interpretacijom Gödelovog drugog teorema nepotpunosti. Prvo je potrebno razlikovati pojedinu teoriju (“sintaksu”) od modela te teorije (“semantiku”). Teorija je zadana aksiomima i pravilima izvođenja: teorije ne znaju ništa o našoj intendiranoj (ili bilo kojoj drugoj) interpretaciji, osim onoga što je eksplicitno ugrađeno u sintaksu (u aksiome i pravila izvođenja). Ako pogledamo neku uobičajenu aritmetičku teoriju, među njenim je aksiomima formula x + 0 = x. Interpretiramo li simbol ‘+’ kao operaciju zbrajanja a simbol ‘0’ kao prirodni broj nulu, imamo istinitu tvrdnju (zbroj bilo kojeg broja i nule je broj s kojim smo krenuli). Ali, interpretiramo li simbol ‘+’ kao operaciju spajanja tekstova a simbol ‘0’ kao prazan tekst, ponovno dobivamo istinitu tvrdnju (ako na bilo koji tekst nadodamo prazan tekst, dobivamo tekst s kojim smo krenuli). Niti u principu nije moguće dodati dovoljno aksioma kojima bi se mogla fiksirati jedna interpretacija (barem ako promatramo teorije prvog reda). Zbog toga svaka teorija nužno ima više modela: više je mogućih struktura koje se ponašaju u skladu s njenim aksiomima i pravilima izvođenja (npr. ako imamo teoriju s jed(i)nim aksiomom “x + 0 = x”, onda je jedan od modela te teorije skup svih prirodnih brojeva uz operaciju zbrajanja, a još jedan model je skup svih tekstova uz operaciju nadovezivanja.) Sve te strukture kao svoje članove (domena nad kojom kvantificiramo kad kažemo “postoji x …” ili “za svaki x …”) imaju “objekte nalik brojevima”, ali neki od tih objekata u nekim od tih struktura ne moraju zaista i biti brojevi.
Modeli uobičajenih formalnih aritmetika ipak imaju korisno svojstvo da su ili jednaki (izomorfni) stvarnim prirodnim brojevima, ili u nekom smislu proširuju skup prirodnih brojeva novim elementima. U potonjem slučaju, obično se zamišlja da ti modeli sadrže stvarne prirodne brojeve (zapravo sadrže neku prirodnim brojevima izomorfnu strukturu) te neke nove brojeve koji su “beskonačno” (ili bolje, neizmjerno) veći od stvarno postojećih prirodnih brojeva. Naravno, ti veliki objekti nisu doslovno “brojevi” (što god to značilo), već neki objekti koji se u nekim aspektima ponašaju nalik brojevima. Uobičajen naziv za objekt koji je neizmjerno veći od stvarnih brojeva je nestandardni broj.
Između sintakse (teorija) i semantike (modeli teorija) postoji jaka veza, u slučaju teorija prvog reda. Veza se zove semantička potpunost (češće samo “potpunost”), i taj pojam nema nikakve veze s pojmom formalne potpunosti. Jednu od prvih verzija dokaza semantičke potpunosti dao je upravo Gödel. Današnja je uobičajena formulacija nešto jača od njegove i kaže da je nešto dokazivo u teoriji (prvog reda) T ako i samo ako je to ispunjeno u svim modelima teorije T. Netrivijalan smjer u dokazu je: ako neka tvrdnja A nije dokaziva u teoriji T, kako utvrditi da postoji model teorije T u kojem vrijedi ne-A? Teorem semantičke potpunosti (za teorije prvog reda) kaže da to uvijek možemo utvrditi, a daje i nešto donekle nalik na algoritam za konstrukciju modela nedokazivih formula (ne postoji, niti je moguć, pravi algoritam).
Prejaka Gödelova formalizacija konzistentnosti?
Vratimo li se na Con(T):
Za svaki d vrijedi: d ne kodira dokaz u teoriji T toga da 0 = 1;
sad možemo komentirati (barem navodni) problem. U standardnom modelu aritmetike (model samo prirodnih brojeva), jasno je (bilo bi jasno kad bi se raspisalo) da Con(T) dobro korespondira s našom idejom konzistentnosti teorije. No, u nestandardnim modelima aritmetike, kvantifikacija “za svaki d” na početku formule Con(T) prolazi i po nestandardnim brojevima (“neizmjerno velikim brojevima”). Pojam kodiranja za takve objekte ima drugačije značenje od standardnog. To značenje se može razlikovati i među različitim nestandardnim modelima aritmetike. Tvrdnja da (nestandardno) kodiranje nestandardnih brojeva (što god to bilo) nikad ne kodira dokaz da 0 = 1 bitno je jača od tvrdnje da prirodni brojevi (koji mogu samo standardno kodirati samo stvarne dokaze) ne kodiraju dokaz da 0 = 1.
Zašto su nam nestandardni modeli i njihovi nestandardni kodovi uopće relevantni, ako nas zanimaju samo prirodni brojevi i standardni kodovi? Iz teorema potpunosti slijedi da je nešto dokazivo samo ako je istinito u svim modelima. Stoga, ako je moguće dokazati Con(T), onda Con(T) mora biti istinita i u svim nestandardnim modelima. Dakle, dokazati tvrdnju o standardnom kodiranju (poput tvrdnje Con(T)) znači dokazati nešto i o nestandardnim kodiranjima. A to je bitno više od onoga što nas zanima: mi želimo dokazati samo da stvarno mogući dokazi ne dokazuju to da 0 = 1, ne smeta nas što neka generalizacija kodiranja na nepostojećim brojevima možda kodira “dokaz” kontradikcije. Gödelov drugi teorem pokazuje da nije dokaziva tvrdnja – tvrdnja Con(T) – koja između ostalog tvrdi nešto o nestandardnim modelima i to je, može se tvrditi, upravo razlog njezine nedokazivosti. Gödelov drugi teorem nepotpunosti, dakle, dokazuje da nije dokaziva neka tvrdnja koja je međutim bitno jača od tvrdnje koja nas je u početku zanimala, a koja nije imala (barem ne na prvi pogled) nikakve veze sa nestandardnim modelima. To znači da je Gödelov rezultat slabiji nego što bismo htjeli (poput strawmana, pobija nešto jače nego što je trebalo pobiti). To tvrdi Artemov.
U napomeni (na dnu) je malo dulji komentar o nestandardnim modelima.
Možemo vidjeti da je aritmetika konzistentna “izvana”: kad ne bi bila, postojanje prirodnih brojeva bi bila besmislica, a mi znamo da prirodni brojevi u nekom smislu (za neke filozofe matematike doslovnom) postoje. Kad bismo se uspjeli riješiti nestandardnih interpretacija, u svim interpretacijama (u “svim” bi tada značilo “u našoj jed(i)noj”) bi bila istinita konzistentnost aritmetike, pa bi (iz teorema potpunosti) konzistentnost bila i dokaziva. Ali, kao što je već komentirano, ne možemo se riješiti nestandardnih modela. Iz tog razloga teorija T ne može dokazati univerzalnu kvantifikaciju u rečenici Con(T), pa stoga niti samu tvrdnju Con(T).
Kako drugačije predstaviti konzistentnost?
Iz teorema potpunosti slijedi da je u nekom nestandardnom modelu istinito da je dokazivo da je aritmetika inkonzistentna (to naravno ne povlači da aritmetika nije konzistentna, baš zato što se radi o nestandardnom modelu). Ne možemo se riješiti nestandardnih modela, ali možemo se riješiti univerzalne kvantifikacije.
Umjesto tvrdnje Con(T):
Za svaki d vrijedi: d ne kodira dokaz u teoriji T toga da 0 = 1;
možemo razmotriti shemu tvrdnji ConSchema(T) koja ima beskonačno mnogo instanci, po jednu za svaki stvarno postojeć prirodan broj:
0 ne kodira dokaz u teoriji T toga da 0 = 1,
1 ne kodira dokaz u teoriji T toga da 0 = 1,
2 ne kodira dokaz u teoriji T toga da 0 = 1,
3 ne kodira dokaz u teoriji T toga da 0 = 1,
…
Čak i u nestandardnim modelima, eksplicitno (npr. tzv. numeralima) zapisani brojevi 0, 1, 2, … preslikavaju se u stvarne prirodne brojeve (odnosno, što je dovoljno dobro, u neku izomorfnu vaijantu stvarnih prirodnih brojeva). Dok je u standardnom modelu (model samo prirodnih brojeva) ekvivalentno tražimo li istinitost za Con(T) ili istinitost (odjednom svih) tvrdnji iz ConSchema(T) (oboje je, naravno, istinito u standardnom modelu), u nestandardnim modelima je Con(T) strogo jača tvrdnja jer traži da ni nestandardni brojevi ne kodiraju dokaze u teoriji T toga da 0 = 1. (Shemu ConSchema(T) definiramo u “našem svijetu”, pa kad se pitamo jesu li sve njene instance istinite u nestandardnom modelu, to su i dalje samo instance za brojeve 0, 1, 2, itd., ne i instance za nestandardne brojeve)
Artemov tvrdi da želji da se pronađe “dokaz konzistetnosti aritmetike” zapravo odgovara dokaz da ne postoji (stvaran broj) kod dokaza koji “kodira neki dokaz za 0 = 1”. Odnosno, da svaki mogući (stvaran broj) kod dokaza “nije kod dokaza za 0 = 1”. Evo nekoliko osnova koje se između ostalog mogu pronaći u članku (Artemov), a koje idu u prilog opisanoj shematskoj formalizaciji konzistentnosti aritmetike:
- Rečenica Con(T), baš stoga što je formalno nezavisna (niti je dokaziva ona, niti njena negacija), traži da se dokaže više od same tvrdnje Con(T) u standardnom modelu: traži da se dokaže nešto o nestandardnim brojevima. Dakle, to je strogo više od onoga što smo trebali dokazati. S druge strane, ConSchema(T) sigurno ne tvrdi ništa više od onoga što smo htjeli dokazati (doduše, možda tvrdi manje, to je diskutabilno).
- Korištenje shema umjesto jedne formule nije “varanje”. Najpopularnija aksiomatizacija aritmetike, Peanova aritmetika prvog reda, princip indukcije formalizira shemom principa. Princip indukcija (u jednoj varijanti) je princip koji kaže da ako (prvo) broj 0 ima neko svojstvo P, te (drugo) ako pod pretpostavkom da proizvoljno odabran broj n ima svojstvo P, onda i broj n + 1 ima svojstvo P; tada svi brojevi uopće imaju dano svojstvo. Princip indukcije ima ulogu konačne aproksimacije takozvanog ω-pravila, pravila zaključivanja koje kaže da iz toga da broj 0 ima svojstvo P, broj 1 ima svojstvo P, broj 2 ima svojstvo P, itd. (po jedna takva tvrdnja za svaki prirodan broj) slijedi tvrdnja da svi brojevi imaju svojstvo P. Kako imamo konačno mnogo vremena i prostora za dokazivanje, ne možemo koristiti ω-pravilo u praksi (iako možemo analizirati “dokaze” koji ga koriste na jednak način na koji analiziramo, primjerice, realne brojeve, unatoč činjenici da i takvi dokazi i realni brojevi mogu sadržavati beskonačnu količinu informacija). Princip indukcije je strogo slabiji od ω-pravila (npr., upravo je konzistentnost uobičajenih matematičkih teorija nešto što ω-pravilo dokazuje, a princip indukcije ne). No, i sam je princip indukcije previše snažan za teorije prvog reda. Naime, princip tvrdi da nešto vrijedi za sva svojstva P. U teorijama prvog reda ne možemo kvantificirati nad svojstvima (već samo brojevima, ili preciznije, objektima-nalik-brojevima). To se uobičajeno rješava tako da umjesto samog principa indukcije, u teoriju dodamo beskonačno mnogo aksioma koji su sve moguće instance sheme principa indukcije. Primjer jedne instance sheme matematičke indukcije, gdje uzimamo da je svojstvo P parnost: ako je 0 paran broj i za sve x, ako to da je x paran povlači da je x + 1 paran, onda za svaki x vrijedi da je x paran. (Ova konkretna instanca beskorisna za dokaze jer, naravno, iz parnosti parnog broja ne slijedi parnost njegovog sljedbenika, neparnog broja, ali jest instanca sheme i stoga aksiom uobičajenih aritmetika.) Za svako moguće svojstvo (poput parnosti, ali proizvoljno kompleksno), shema aksioma indukcije dodaje po jedan aksiom. Dakle, matematičari uobičajeno formaliziraju indukciju shematski ako rade u aritmetici prvog reda. Artemov predlaže da se tako radi i sa konzistentnosti.
- Za teorije prvog reda vrijedi svojstvo kompaktnosti. To svojstvo kaže da ako je neka rečenica R posljedica nekog (možda beskonačnog) niza rečenica A1, A2, A3, …, onda postoji neki (naravno, stvaran) prirodan broj n takav da je R posljedica već samo konačnog skupa rečenica A1, …, An.
Teorem kompaktnosti naravno ne vrijedi ako rečenicu R u iskazu teorema zamijenimo nekim beskonačnim skupom rečenica R: u tom slučaju nećemo nužno uspjeti pronaći konačan podskup premisa iz kojeg slijedi čitav R.
Pretpostavimo sada da neka uobičajena teorija T dokazuje svoju konzistentnost. Dodatno, pretpostavimo da se radi o teoriji poput Peanove aritmetike, koja nije konačno aksiomatizabilna (ne postoji neki konačan skup aksioma koji bi odjednom zamijenio sve instance sheme principa indukcije). Imamo dakle da T dokazuje Con(T). Iz kompaktnosti slijedi da i neka konačna podteorija, označimo ju kao T’, stoga dokazuje Con(T). Međutim, kako T nije konačno aksiomatizabilna, T’ je (osim što je naravno neusporedivo manja količinom aksioma) ujedno i dokazno strogo slabija od T. Kad T’ ne bi bila dokazno slabija od T, onda bi T’ bila jedna konačna aksiomatizacija za T, a to bi značilo da je T konačno aksiomatizabilna (što nije). Ako bismo inzistirali na tome da je upravo Con(T), a ne ConSchema(T) (ili nešto treće) ispravna formalizacija konzistentnosti, to bi značilo da očekujemo da T’ nekako možda može zaključiti da T ne dokazuje 0 = 1, unatoč činjenici da postoji beskonačno mnogo teorema od T koje T’ uopće ni ne zahvaća (kamoli dokazuje konzistentnost skupa svih teorema od T). Takvo je očekivanje vrlo nerealno, pa pitanje je li to moguće možda i nije pravo pitanje.
Prihvatimo li da formalizacija pomoću ConSchema(T) bolje odgovara na pitanje “je li konzistentnost dokaziva?” od formalizacije pomoću Con(T), mijenja li se išta u odgovoru na to pitanje? Pokazuje se da da: barem u slučaju Peanove aritmetike, dokaz konzistentnosti je moguć (tj. sve instance sheme ConSchema(Peanova-aritmetika) jesu dokazive u Peanovoj aritmetici). To je dijametralno suprotni ishod od formalizacije s Con(T) za bilo koju teoriju T: ne samo da Con(T) nije dokaziva u T, već štoviše svaka uobičajena teorija T dokazuje da: dokazuje Con(T) samo ako je T inkonzistentna (vidi napomenu 6).
Gödelov drugi teorem nepotpunosti odnosi se na vrlo velik broj teorija T, ne samo Peanovu aritmetiku. Za njih ostaje otvoreno pitanje dokazuju li ConSchema(T), odnosno utječe li njegova drugačija formalizacija na odgovor na pitanje o dokazivosti konzistentnosti. To je, naravno, matematičko pitanje koje je barem u principu neovisno o uvjerenjima i raspravama. Bitno je istaknuti da nikakva rasprava oko toga što je bolja formalizacija nimalo ne utječe na matematičku korektnost ili relevantnost Gödelovih teorema, kao niti teorema vezanih uz shemu ConSchema(T). Vjerojatno bi se moglo tvrditi da je čak i filozofska važnost Gödelove formalizacije neovisna o eventualnoj većoj plauzibilnosti formalizacije u obliku ConSchema(T) (jer ima brojne druge posljedice na matematiku i izvan originalne motivacije). U svakom slučaju, ono što može biti (i jest) predmet rasprave filozofske je prirode: koja formalizacija bolje odgovara na pitanje može li teorija dokazati svoju konzistentnost? Što bi bili potencijalni odgovori nekoga tko smatra da je Con(T) adekvatnija formalizacija?
Prvo, ako teorija T može dokazati Con(U), onda može zaključivati o toj tvrdnji. Primjerice, može dokazati tvrdnje poput “T dokazuje da T dokazuje da T dokazuje da Con(U)“. Malo zanimljivije, može se dokazati da je u T i tvrdnja “Con(Con(U)) povlači Con(U)” dokaziva. Takve “introspektivne” tvrdnje nisu direktno izvedive s alternativnom formalizacijom. Posve je jasno da nije moguće dokazati “T dokazuje da T dokazuje da T dokazuje da ConSchema(U)“, jer ConSchema(T) predstavlja beskonačno mnogo svojih instanci (a ne jednu formulu). Moguće su neke alternativne formalizacije tvrdnje “teorija U dokazuje sve instance sheme ConSchema(T)” poput, možda, CCon predikata u članku. No, jasno je da što god napravili, izgubljen je status jedne tvrdnje koju se može (ako se može) dokazati, i o njoj zaključivati. Kao što Artemov uočava, kod indukcije nam to nije strašno smetalo. Međutim, da smo umjesto sheme indukcije mogli uključiti čitav princip indukcije, to bismo i napravili. Nismo uključili čitav princip indukcije isključivo zato što logika prvog reda ne može kvantificirati svojstva.
Drugo, čini se da je nekakva pozadinska implikacija kritike koju daje Artemov na standardnu formalizaciju to da su nestandardni modeli uzrok nedokazivosti (klasično formalizirane) konzistentnosti. Nestandardni modeli su nešto što želimo izbjeći, pa je u redu izbjegavati ih. Međutim, to je samo jedna perspektiva na “uzroke” fenomena nepotpunosti. Nestandardni modeli, zanemarimo li to što ih zovemo “nestandardnima”, neizbježni su. To znači da su oni barem u nekom smislu integralan dio matematike (dok ih Artemov komentira kao “logical technicality”). Možda bi neka druga perspektiva (različita od priče oko modela aritmetike) išla u prilog tome da je Con(T) bolja formalizacija? Teško je (ili barem teško meni u ovom trenutku) zamisliti perspektivu u kojoj bi Con(T) bio išta više od blago problematične formalizacije. Za ConSchema(T) mi problematičnost djeluje izglednijom, dijelom jer se toliko oslanja na eksterni “kvantifikator” (za svaki prirodni broj n, po jedna instanca) i standardni model, a dijelom naprosto jer se radi o shemi.
Nemam izražen stav ni o (filozofskim) tvrdnjama Artemova niti o ova dva potencijalna smjera odgovora; mislim da sve napisano ima neku dozu uvjerljivosti. Mislim da mi se zasad najviše sviđa stav da pitanje “je li konzistentnost dokaziva?” nije dovoljno precizno, pa su (mi) stoga i različite formalizacije uvjerljive.
Napomene
(1) Vezano uz “uobičajene teorije” i doseg Gödelovih teorema. U prethodnom tekstu ukratko je objašnjeno što se tu misli pod “uobičajene” (tamo “pogodne”). To nije posebno relevantno jer su sve teorije unutar kojih se radi ili može raditi neka stvarna matematika pogođene ovim fenomenom. Ne može postojati trik kojim bi se Gödelovi teoremi mogli izbjeći. Jedna potencijalno zanimljiva a formalno potpuna teorija (dakle teorija koja očito nije zahvaćena Gödelovim prvom teoremom) je teorija realnih brojeva prvog reda (s teoremima poput “za svaki x za koji postoji neki y takav da y * y = x, postoji i neki z takav da z * z * z * z = x”). Ta je teorija (RCF ili RCOF) ipak preslaba da bi se u njoj radila zanimljiva matematika. Naime, jedno od temeljnih svojstava realnih brojeva, princip da svaki rastući niz brojeva koji je odozgo ograničen ima limes, nije uopće izraziv u jeziku te teorije (jer se radi o svojstvu drugog reda). Konkretan uvjet koji ova teorija ne ispunjava, a koji je nužan u dokazu Gödelovih teorema, je nedostatak izražajnosti, ili preciznije, sekvencijalnosti. Naime, ta teorija niti u principu ne može izraziti svojstva konačnih listi (konačnih nizova, finite sequences). Gödelovi dokazi kodiraju formalnu aritmetiku (i druge teorije) koristeći objekte tih teorija (npr. brojeve). Između ostalog, mora se pronaći način za govor o samim formulama i dokazima. Formule su konačni nizovi simbola, a dokazi konačni nizovi formula. Dio Gödelovih dokaza su pomoćne tvrdnje poput te da ako spojimo (konkateniramo) dva dokaza, opet ćemo dobiti nekakav (možda besmislen) dokaz. Na takvim je mjestima potrebna sekvencijalnost: mogućnost govora o konačnim listama. RCOF ne može izraziti niti bitno trivijalnije koncepte od konačnih listi, poput nekakvog koncepta prebrojavanja. Primjerice, tvrdnja da svaki prirodni broj ima sljedbenika također nije izraziva, pa posebno ni dokaziva.
(2) Vezano uz to je li kontroverzna tvrdnja da su “matematičari dokazali da ne postoji najveći prost broj.” Naravno, moguće je na puno načina prigovoriti toj tvrdnji. Primjerice, ta tvrdnja sadrži neograničenu kvantifikaciju (ne tvrdimo samo “ne postoji x manji od y, takav da je x najveći prost broj”, već “ne postoji x, ma kako velik, takav da je x najveći prost broj”), pa bi netko mogao argumentirati da je sama tvrdnja besmislena jer implicitno pretpostavlja da ima smisla govoriti o proizvoljno velikim brojevima. No u kontekstu formalizacije metamatematičkih tvrdnji javljaju se problemi oko kojih su nejasnoće barem za magnitudu veće od ovakvih situacija.
(3) Gentzenov teorem. Ovaj teorem, i teoremi sličnog oblika, dokazuje konzistentnost raznih matematičkih teorija. Matematički, to nisu problematični rezultati, tj. nemaju grešaka. Ali filozofski, ili u nekom širem matematičkom smislu, nije jasno kako oni utječu na naše razumijevanje problema konzistentnosti. Naime, ti su dokazi konzistentnosti provedeni unutar teorija koje su strogo snažnije od teorija čiju konzistentnost dokazuju. Ako je teorija A inkonzistentna, onda je i teorija A proširena nekim aksiomom B barem jednako problematična koliko i teorija A. Gentzenov je rezultat svakako “filozofski” relevantan ako i ne mislimo da nam daje argument da je neki dio matematike konzistentan. Naime, taj tip dokaza lijepo izražava koliko su nam točno jake pretpostavke potrebne da bismo dokazali da je konzistentna teorija doista konzistentna. U odnosu na tu mjeru možemo i rangirati teorije: jače teorije traže jače pretpostavke. Zanimljivo je da ove jakosti možemo mjeriti tzv. ordinalnim brojevima, generalizacijom ideje rednog broja. Primjerice, uobičajenim formalizacijama aritmetike pripada ordinalni broj koji se označava kao ε0. Nakon svih običnih rednih brojeva (prvi, drugi, treći, …) dolazi broj koji se označava kao ω, pa ω + prvi, ω + drugi, … Na kraju tog niza, slijedi ω * dva, … ω * dva + prvi, … I tako dalje: ω * tri, …, ω * ω = ω2, ω2 + prvi, …, ω2 + ω, …, ω2 * 23 + ω * 50 + stoti, …, ω3 , …, ω4 …, ω5 , …, ωω , …nastavimo li dalje graditi ordinalne brojeve (ω potencirano na ωω, pa ω potencirano na to itd.), prvi broj veći od svih brojeva takvog oblika je upravo ε0. Za neke je teorije odgovarajući (ordinalni) broj puno manji ili puno veći.
(4) Napomena oko “otpakiravanja” Gödelovog drugog teorema nepotpunosti. Postoje barem dvije verzije Gödelovog drugog teorema nepotpunosti. Slabija (ali uobičajena) verzija kaže: “Ako T dokazuje svoju konzistentnost, onda T nije konzistentna.” Jača (tzv. “formalizirana”) verzija kaže da slabija verzija ne samo vrijedi, već je i dokaziva unutar (opet) same teorije T. Preciznije, jača verzija kaže: “Teorija T dokazuje sljedeći kondicional: ako teorija T dokazuje konzistentnost, onda teorija T dokazuje kontradikciju”. Drugim riječima, teorije ne samo da ne mogu dokazati svoju konzistentnost, već su sposobne i same dokazati da ne mogu dokazati svoju konzistentnost. Mogli bismo reći da ne samo da su ograničene, već su i svjesne svojih ograničenja. Formalizirana verzija je doista jača: neke (pre)slabe teorije ne mogu dokazati svoju konzistentnost, ali ne mogu same dokazati da ju ne mogu dokazati svoju konzistentnost (na njih se Gödelovi teoremi ne odnose, jer zbog svoje slabosti ne spadaju u “uobičajene” teorije; teorije na koje se odnose Gödelovi teoremi ispunjavaju i običnu i formaliziranu verziju teorema). Za “vidjeti” da u tim slabim teorijama nije dokaziva njihova konzistentnost potrebna je neka teorija jača od njih.
(5) Napomena o utjecaju nestandardnih modela na uobičajenu matematiku. Ako su nestandardni modeli toliko problematični, kako to da ne utječu i na uobičajene matematičke dokaze? Tj. zašto matematičari ne moraju osigurati da njihovi teoremi vrijede i u nestandardnim modelima? U tekstu opisani problemi s nestandardnim brojevima relevantni su zapravo samo u slučaju rečenica oko kojih se teorija ne može odlučiti (“formalno nezavisnih” rečenica, tj. takvih da niti one niti njihove negacije nisu dokazive). Naime, ako je tvrdnja dokaziva, istinita je u standardnom modelu. Kad dokažemo nešto kao “ne postoji najveći prost broj”, tada znamo da je to istinito i za prirodne brojeve. Naravno, usput smo dokazali i neke vrlo egzotične tvrdnje o nestandardnim brojevima u nestandardnim modelima. No, to nas ne smeta, jer smo dokazali i ono što smo htjeli (da tvrdnja vrijedi i za prirodne brojeve). Posve analogno, ako je negacija neke promatrane rečenice dokaziva, njena negacija je istinita i u standardnom modelu. Vidimo da se u ta dva slučaja nije bilo potrebno obazirati na postojanje nestandardnih modela. Za uvjerljivu većinu matematičarima relevantnih aritmetičkih rečenica vrijedi da su one ili njihove negacije doista dokazive u uobičajenim teorijama (većina i u vrlo slabim verzijama tih teorija). Iz tog smo razloga i rijetko svjesni problema koje nestandardni brojevi mogu izazvati. Vrlo je mali broj formalno nezavisnih rečenica koje nisu duboko vezane uz metamatematiku, odnosno koje se prirodno javljaju u teoriji brojeva. Iz tog razloga nas ne smeta što rečenicu “svaki broj nije najveći prost broj” formalizirali formulom koja počinje univerzalnim kvantifikatorom (iako će kvantifikacija “za svaki” uključiti i nestandardne brojeve, rečenica je dokaziva, pa nas ne smeta što smo dokazali i malo više nego što smo htjeli), ali nas smeta smo što rečenicu “aritmetika je konzistentna” formalizirali formulom koja počinje univerzalnim kvantifikatorom (jer ovdje nas upravo nestandardni brojevi blokiraju u završavanju dokaza). Kad se dogodi situacija da je neka rečenica nezavisna, tek tada ima smisla želja da se riješimo nestandardnih modela.
(6) Treba razlikovati tvrdnje “kad bi teorija T dokazivala Con(T), bila bi inkonzistentna” (što je Gödelov drugi teorem nepotpunosti) te “teorija T proširena s Con(T) kao aksiomom jest inkonzistentna” (što općenito ne vrijedi.) U potonjem slučaju imamo teoriju T + Con(T) koja ne mora biti inkonzistentna. Naime, ta teorija ne dokazuje svoju konzistentnost: njena konzistentnost nije tvrdnja Con(T), već tvrdnja Con(T + Con(T)). Ta složenija tvrdnja ostaje nedokaziva i u teoriji T + Con(T). Teorija T + Con(T) doista dokazuje konzistentnost neke teorije, ali ne sebe same, već jedne svoje podteorije: teorije T (dokaz konzistentnosti teorije T u teoriji T + Con(T) je trivijalan, konzistentnost teorije T je očito aksiom teorije T + Con(T)). Slično, možemo napraviti daljnje proširenje: T + Con(T) + Con(T + Con(T)). Ova teorija trivijalno dokazuje konzistentnost teorija T i T + Con(T), ali ne dokazuje svoju konzistentnost, tj. ne dokazuje tvrdnju Con(T + Con(T) + Con(T + Con(T))).
nagovor na filosofiju 