Neprotislovnost klasične sintetične teorije izračunljivostiPutrle, Žiga (Avtor) Bauer, Andrej (Mentor) teorija tipovteorij izračunljivostiteorija realizabilnostidokazovalni pomočnikiYannick Forster v svojem doktorskem delu Computability in constructive type theory predlaga nov sintetični pristop k teoriji izračunljivosti, ki omogoča razvoj teorije na klasičen način s pomočjo dokazovalnega pomočnika. Teorijo izračunljivosti razvije v računu induktivnih konstrukcij (RIK) (ang. calculus of inductive constructions), ki je osnova dokazovalnega pomočnika Coq, in predpostavi, da lahko v RIK-u uporabimo sintetično Churchevo tezo (SCT), zakon izključene sredine (ZIS) in pravila velike uporabe (PVU), ne da bi s tem uvedli protislovje. Predpostavko zagovarja s sklicevanjem na podobne že dokazane rezultate, vendar dokaza neprotislovnosti ne poda. Naš prispevek k Forsterjevemu delu je dokaz, da je sintetična teorija izračunljivosti, ki jo razvije v RIK-u + SCT + ZIS + PVU, neprotislovna. Osredotočimo se na del RIK-a, ki ga Forster uporablja pri razvoju teorije, in ga imenujemo fRIK. Podamo dva dokaza neprotislovnosti fRIK-a + SCT + ZIS + PVU. V prvem dokazu sodbe sistema fRIK + SCT + ZIS + PVU sintaktično preslikamo v sodbe sistema fRIK + SCT + PVU, kjer vse logične izjave nadomestimo z njihovo stabilno obliko in se tako izognemo aksiomu ZIS. Nato zgradimo model fRIK + SCT + PVU v teoriji realizabilnosti. V drugem dokazu zgradimo model fRIK + SCT + ZIS + PVU direktno. V modelih odvisne tipe interpretiramo kot družine skupkov, svet logičnih izjav P kot skupek ⠇Per(K1), kjer je Per(K1) kategorija delnih ekvivalenčnih relacij nad Kleenejevo prvo algebro K1, in svet stabilnih logičnih izjav P¬¬ kot skupek ⠇2, kjer je 2 množica skupkov 0 in 1.20232023-12-16 08:15:03Magistrsko delo/naloga153088VisID: 139634COBISS_ID: 177554179sl