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:

Formule modalne logike definiraju se rekurzivno:

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

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

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

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.

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.

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.

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

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:

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

Sada ćemo precizirati vezu logike dokazivosti i aritmetike.

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

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?”

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.

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.

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:

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.

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.

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.

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.

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.

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.

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:

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

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.

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

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

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.

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}