20.500.12556/RUL-153088 Neprotislovnost klasične sintetične teorije izračunljivosti magistrsko delo Consistency of classical synthetic computability theory Yannick 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. In his doctoral thesis Computability in constructive type theory, Yannick Forster suggests a new synthetic approach towards computability theory that allows development of the theory in a classical way by using proof assistants. He develops the theory within calculus of inductive constructions (CIC), the underlying type system of Coq proof assistant. He assumes that in CIC we can use synthetic Church’s thesis (SCT), law of excluded middle (LEM) and rules of large elimination (RLE) without making the theory inconsistent. He justifies his assumption by referencing similar proven results, but he does not provide a proof. Our contribution to Forster’s work is a proof that synthetic computability theory developed in CIC + SCT + LEM + RLE is consistent. We focus on a fragment of CIC that Forster uses to develop the theory and name it fCIC. We prove the consistency of fCIC + SCT + LEM + RLE in two ways. First, we syntactically map judgments from fCIC + SCT + LEM + RLE to fCIC + SCT + RLE, where we replace logical propositions with their stable form which allows us to avoid ZIS. Then we build a model of fCIC + SCT + RLE in the theory of realizability. In the second proof, we build the model of fRIK + SCT + ZIS + RLE directly. We model dependent types as families of assemblies, universe of propositions P as assembly ⠇Per(K1), where Per(K1) is a category of partial equivalence relations over Kleene’s first algebra K1, and the universe of stable propositions P¬¬ as an assembly ⠇2, where 2 is a set of assemblies 0 and 1. teorija tipov teorij izračunljivosti teorija realizabilnosti dokazovalni pomočniki type theory computability theory realizability theory proof assistants true false false Slovenski jezik Angleški jezik Magistrsko delo/naloga 2023-12-16 08:15:03 2023-12-16 08:15:09 2024-05-29 12:44:43 0000-00-00 00:00:00 2023 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 139634 177554179 11988.pdf 11988.pdf 1 AAD71E850B545F8B05BC44651DE652DB ae4b68ab76a1007e4d206a2690753106b889c5cb141b042c3f9c914f4c07aeb3 d972703c-9be2-11ee-86ca-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=178944 Fakulteta za matematiko in fiziko Fakulteta za računalništvo in informatiko 0 0 0