This repository contains the master's thesis Consistency of classical synthetic computability theory (sl. Konsistentnost klasične sintetične teorije izračunljivosti) prepared by Žiga Putrle under the supervisor of prof. dr. Andrej Bauer at University of Ljubljana - Faculty of Mathematics and Physics.
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.
The master thesis can be found in the current directory under the name zputrle_masters_thesis_2023.pdf.
The proof/code written in Agda related to the thesis can be found in src/PropNotNot.agda file.
In order to type-check the code in src/PropNotNotInAgda, you also need to checkout the agda-lib submodule. For the initial checkout of the repository, you can use
git clone --recurse-submodules [email protected]:zputrle/master-thesis.git