Ak. god. 2025./2026.

Logika interpretabilnosti IL proširuje logiku dokazivosti GL. Osnovna semantika za IL je Veltmanova semantika. Poznato je da je logika IL potpuna u odnosu na Veltmanovu semantiku, ali isto se ne može reći za njezina proširenja, od kojih su neka dokazano nepotpuna.

U ovom izlaganju definirat ćemo novu klasu Booleovih algebri koje se mogu koristiti za modeliranje logika interpretabilnosti. Ove algebre na prirodan način proširuju modalne algebre i mogu se smatrati generalizacijama Veltmanovih okvira. Dodatno, svako konzistentno proširenje IL adekvatno je i potpuno obzirom na ovu semantiku.

Danas su u analizi preostali samo prirodni brojevi ili sustavi prirodnih brojeva… Matematika je aritmetizirana. (Poincaré, 1900.)

U potrazi za sigurnim temeljem matematike, matematičari su se okrenuli prirodnim brojevima. Iz njih i njihovih skupova izgradili su realne i kompleksne brojeve, funkcije i geometrijske objekte. Pitanja o njima preveli su u pitanja o ℕ i 𝒫(ℕ). To je projekt aritmetizacije koji je Kronecker odbacio kao „mistiku.“

Hilbert je predložio program aksiomatskog opravdanja te „mistike“ tako da se analiza razvije u okviru aksiomatskog sustava realnih brojeva te da se konzistentnost tog sustava dokaže konstruktivnim metodama koje bi Kronecker prihvatio (to je bio Hilbertov drugi problem).

Gödel je 1931. dokazao da je tako formulirano pitanje konzistentnosti formalnog aksiomatskog sustava analize ekvivalentno odgovarajućem pitanju u formalnom aksiomatskom sustavu aritmetike, npr. PA, ali je također dokazao da se na to pitanje u PA ne može odgovoriti (ni konzistentnost samog sustava PA nije dokaziva u PA).

Zato nije pretjerano reći da su moderna logika i izračunljivost proizašle iz zabrinutosti matematičara 19. stoljeća za temelje analize.

Drugi su matematičari, paralelno, slijedili Kroneckera u izgradnji analize konstruktivnim metodama. Jedan od slavnijih bio je Herman Weyl koji je 1918. izgradio analizu u sustavu s aksiomom aritmetičke komprehenzije. Danas bismo rekli u sustavu ACA₀. Taj je sustav dovoljno jak da dokaže sve temeljne teoreme analize. On je i PA konzervativan pa ga to kvalificira kao istinsku aritmetizaciju analize.

No nije da aritmetička komprehenzija samo dokazuje ove teoreme. Ona je zapravo ekvivalentno nekima od njih i te se ekvivalencije mogu dokazati u RCA₀ (sustavu izračunljive analize). Time se bavi reverse mathematics u kojoj su se iskristalizirali sustavi RCA₀, WKL₀, ACA₀, ATR₀ i Π₁¹CA₀. Oni su poznati kao “velika petorka” i generiraju gotovo sve teoreme standardne matematike.

Teoremi najjačih sustava ATR₀ i Π₁¹CA₀ imaju ,,skupovni štih” (kakav npr. ima Cantor-Bendixsonov teorem koji tvrdi da je neprebrojiv zatvoreni skup uvijek unija prebrojivog i savršenog skupa). Takvi teoremi su na marginama “uobičajene” analize pa bi analitičari mogli biti zadovoljni teorijama RCA₀ ⊂ WKL₀ ⊂ ACA₀. Ipak, neki važni dijelovi kombinatorike premašuju ACA₀.