| Sažetak (hrvatski) | Tema ove disertacije su logike interpretabilnosti, koje opisuju ponašanje predikata interpretabilnosti. Prvo ćemo nešto reći o interpretacijama između teorija. Postoji nekoliko verzija interpretacija u upotrebi, ali ono što je zajedničko svima jest da se radi o preslikavanju koje čuva strukturalna svojstva. To preslikavanje preslikava formule interpretirane teorije u formule interpretirajuće teorije. Za ovo se preslikavanje zahtijeva da u nekoj mjeri očuva dokazivost, tj. ako je A aksiom interpretirane teorije, onda slika formule A mora biti dokaziva u interpretirajućoj teoriji. Zahtjev da preslikavanje čuva strukturalna svojstva znači da komutira s propozicionalnim veznicima. Za kvantificirane se formule dopušta malo odstupanje prilikom interpretacije; konkretno, moguće je ograničiti domenu (svih) kvantificiranih formula koristeći unaprijed određen predikat kojeg zovemo specifikator domene (tj. zanima nas relativizirana interpretabilnost). Ovo nam omogućuje izgradnju, primjerice, teorije brojeva u teoriji skupova, gdje (u uobičajenoj konstrukciji) samo neki skupovi predstavljaju brojeve. Možemo zahtijevati da su aksiomi interpretirane teorije dokazivi u interpretirajućoj teoriji, ali možemo to zahtijevati i za sve teoreme uopće interpretirane teorije (razlika je bitna samo kada se radi u slaboj metateoriji). Logike interpretabilnosti opisuju ponašanje određene verzije interpretabilnosti. Za po- četak, ograničavamo se na teorije prvoga reda. Drugo, zanima nas samo interpretabilnost između konačnih proširenja neke unaprijed određene teorije T. Treće, zanima nas formalizirana interpretabilnost, tj. ne proučavamo problem vrijedi li da T + A interpretira T +B, već se bavimo problemom može li T dokazati da T +A interpretira T +B. Četvrto, ne zanima nas za koje pojedinačne formule A i B vrijedi da T + A interpretira T + B, već nas zanimaju ona svojstva koja su strukturalna u smislu da vrijede za bilo kakav odabir formula A i B. U ovoj se disertaciji odlučujemo za interpretabilnost teorema, tj. za to da T + A interpretira T + B zahtijevamo da svaki prijevod teorema od T + B bude dokaziv u T + A. Teorija T pritom mora biti dovoljno snažna, primjerice sekvencijalna. Ako je takva teorija aksiomatizabilna, onda postoji i predikat \(Int_T(·, ·)\), definiran na prirodan način, koji izražava svojstvo da je prvi argument predikata interpretira drugi argument. Logika interpretabilnosti teorije T definira se na sličan način kao i logika dokazivosti teorije T, ali s dodanim binarnim modalnim operatorom \(\triangleright\) čija je intendirana interpretacija \(Int_T\) . Dakle, logika interpretabilnosti teorije T jest skup svih modalnih formula u jeziku logike interpretabilnosti koje su dokazive za koju god aritmetičku interpretaciju propozicionalnih varijabli te preslikavajući modalne operatore u njihove intendirane aritmetizacije. Logika interpretabilnosti teorije T ovisi o teoriji T. Primjerice, logika interpretabilnosti Gödel–Bernaysove teorije skupova (što je logika koju označavamo kao ILP), i logika interpretabilnosti Peanove Aritmetike (što je logika koju označavamo kao ILM), razlikuju se. Za sekvencijalnu teoriju T postoji određeni skup formula, koji se obično označava kao IL(All), kojeg logika interpretabilnosti bilo koje teorije T mora sadržavati. Točan sadržaj skupa IL(All) nije poznat; u stvari, popravljanje donje granice je pitanje koje motivira većinu istraživanja u ovom području. Jedna jednostavna donja granica je osnovna logika interpretabilnosti, koju označavamo s IL. To je proširenje logike dokazivosti koje sadrži pet dodatnih shema aksioma koje se u literaturi označava sa J1–J5. Vraćajući se na pitanje sadržaja skupa IL(All), postoji zanimljiv i iznenađujuć pristup podizanju najbolje poznate donje granice; drugim riječima, traženja novih aritmetički valjanih principa interpretabilnosti. Pristup o kojem je riječ jest proučavanje modalne relacijske semantike. Novi su aritmetički valjani principi otkriveni promatrajući karakteristična svojstva već poznatih principa, modificirajući ih, te određujući modalne formule koje karakteriziraju tako dobivena relacijska svojstva. Ovakav postupak naravno ne garantira aritmetičku valjanost tako otkrivenih modalnih formula, ali neki aritmetički valjani principi doista jesu pronađeni na ovaj način. Još jedan sličan pristup je pokušati dokazati modalnu potpunost određenih proširenja logike IL. Ako dokaz modalne potpunosti ne uspije, daljnje proširivanje spomenutog proširenja, dok god se ne ustanovi modalna potpunost, može rezultirati novim aritmetički valjanim formulama (ovaj će se pristup primijeniti u posljednjem poglavlju ove disertacije). Postoje dva osnovna tipa modalne semantike korištena za logike interpretabilnosti. Jedan je regularna Veltmanova semantika (ili obična Veltmanova semantika, ili samo Veltmanova semantika kad ne postoji mogućnost zabune). Druga je generalizirana Veltmanova semantika koju je uvela Verbrugge, a koja osim osobina relacijske semantike ima i osobine okolinske semantike. Regularnu Veltmanovu semantiku moguće je koristiti za dokaz potpunosti brojnih logika interpretabilnosti. Međutim, za kompleksnije logike, generalizirana semantika može se iskoristiti za dati jednostavnije i razumljivije dokaze potpunosti. Posljednjih godina i posebno tijekom pisanja ove disertacije, generalizirana se semantika pokazala kao posebno dobro primjenjiva relacijska semantika za logike interpretabilnosti. Preciznije, jednostavnije je doći do rezultata o modalnoj potpunosti, a odlučivost se može dokazati koristeći filtracije u svim poznatim slučajevima. Mi dokazujemo različite nove rezultate, a uz to dajemo i nove dokaze starih rezultata, vezane uz potpunost u odnosu na generaliziranu semantiku. U nekim slučajevima znamo samo da je određena logika potpuna u odnosu na generaliziranu semantiku. Štoviše, postoje primjeri logika koje su potpune u odnosu na generaliziranu semantiku, a za koje znamo da su nepotpune u odnosu na regularnu Veltmanovu semantiku. Svi poznati rezultati o složenosti (od kojih se većina dokazuje upravo u ovoj disertaciji) koriste regularnu Veltmanovu semantiku. Što se tiče odlučivosti, čini se da je generalizirana semantika ponovno pogodniji alat, jer omogućava uniformnu metodu dokazivanja svojstva konačnih modela. U ovoj se disertaciji bavimo različitim svojstvima formalizirane relativizirane interpretabilnosti. U središnjem dijelu disertacije bavimo se različitim logikama interpretabilnosti i sljedećim njihovim aspektima: potpunost u odnosu na modalnu semantiku, odlučivost te algoritamska složenost. Osim rezultata koji se tiču same semantike, koristimo semantičke metode kako bismo odredili algoritamsku složenost problema dokazivosti (i konzistentnosti) za različite logike interpretabilnosti. Što se tiče aritmetičkog aspekta, proučavamo tri niza principa interpretabilnosti. Za dva među njima, za koja su aritmetička i modalna adekvatnost već poznati, dajemo nove dokaze aritmetičke adekvatnosti. Treći je niz rezultat naših modalnih razmatranja. Dokazujemo da je aritmetički adekvatan i karakteriziramo klasu okvira u odnosu na običnu Veltmanovu semantiku. Osim toga, razmatramo potpunost nekih logika vezanih uz treći niz (radi se o logikama ILWR i \(ILW_\omega\)). Sad ćemo dati pregled strukture disertacije. U prvom poglavlju dajemo neformalan uvod u okvirno područje kojem pripada ova disertacija. U drugom poglavlju dajemo formalniji uvod, osnovne definicije te dokazujemo neke jednostavnije rezultate. U iduća dva poglavlja istražujemo modalnu potpunost. Prvo uvodimo ključni alat: osiguravajuće oznake. Razvijamo općenitu teoriju osiguravajućih oznaka, uključujući koncept Γ-punih osiguravajućih oznaka. Razvijamo i teoriju koja se koristi kasnije u disertaciji, ali dokazujemo i rezultate zanimljive same po sebi (poput karakterizacije Γ-punih skupova). U četvrtom poglavlju koristimo osiguravajuće oznake kako bismo dokazali potpunost različitih logika interpretabilnosti u odnosu na generaliziranu Veltmanovu semantiku. Definiramo ILX-strukture za \(X \subseteq \{ M, P, M_0, P_0, R \} \) te \(X \subseteq \{ W, W^* \} \) i dokazujemo da je pripadna logika ILX potpuna u odnosu na svoju karakterističnu klasu okvira. Posebno, dokazujemo da su logike \(ILP_0\) i ILR potpune, što su novi rezultati. Također definiramo problem iteracije oznaka i uvodimo specijalan tip struktura, ILWP-strukture, koje rje- šavaju ovaj problem u relativno jednostavnom slučaju logike ILP. Motivacija za ovo istraživanje jest što se problem iteracije oznaka javlja u složenijim logikama poput logike ILWR, gdje je potpuno rješenje zasad nepoznato. Mi vjerujemo da bi isto rješenje moglo biti iskoristivo i za druge složenije logike, ali za to ustvrditi potrebno je riješiti i neke druge probleme. Ponovno se bavimo potpunošću u finalnom poglavlju ove disertacije gdje se, između ostalih rezultata, bavimo dokazom potpunosti logike ILWR pod pretpostavkom postojanja odgovora na neke druge otvorene probleme. U petom poglavlju koristimo dobivene rezultate o potpunosti i dokazujemo odlučivost različitih logika. Ovo je još jedna, i možda najkorisnija, primjena generalizirane semantike: mogućnost uniformne definicije filtracija. Šesto poglavlje bavi se algoritamskom složenošću; dokazujemo da IL, ILW i ILP pripadaju klasi složenosti PSPACE-potpunih problema. Sedmo poglavlje bavi se aritmetičkim aspektima logika interpretabilnosti. Dajemo nov dokaz aritmetičke adekvatnosti nedavno otkrivenih nizova principa interpretabilnosti. U posljednjem poglavlju uvodimo još jedan niz principa interpretabilnosti, dokazujemo mu aritmetičku adekvatnost, i pronalazimo mu Veltmanovu semantiku. Kao što smo već najavili, dajemo i uvjetne dokaze potpunosti za logike koje se tiču novog niza principa interpretabilnosti. |
