Advisors: Yannick Forster
Reducibility is an essential concept for undecidability proofs in computability theory. The idea behind reductions was conceived by Turing, who introduced the later so-called Turing reduction based on oracle machines. In 1944, Post furthermore introduced with one-one, many-one, and truth-table reductions in comparison to Turing reductions more specific reducibility notions. Post then also started to analyze the structure of the different reducibility notions and their computability degrees. Most undecidable problems were reducible from the halting problem, since this was exactly the method to show them undecidable. However, Post was able to construct also semidecidable but undecidable sets that do not one-one, many-one, or truth-table reduce from the halting problem.
This thesis formalizes and mechanizes parts of the traditional one-one, many-one, and truth-table reducibility theory based on a synthetic approach in the constructive type theory of the proof assistant Coq. The core idea of synthetic computability theory is to work in a setting that allows to identify the notion of a function with the notion of a computable function. As a programming language, Coq forms such a synthetic setting by guaranteeing all definable and therefore appearing functions to be immediately computable which avoids complex constructions in an underlying computational model.
We show positive results like Myhill's Isomorphism Theorem, order properties of reductions, and characterize both many-one and truth-table reducibility in terms of one-one reductions in axiom-free Coq. Distinctions of reducibility degrees as stated for instance by Post are in contrast only provable using particular properties of computational models like a universal machine. Constructing such a machine is not possible when working synthetically without a concrete computational model in hand. Assuming however abstract synthetic axioms concerning the computability of functions allows us to prove also negative results synthetically. We follow Post's construction of a simple set and achieve an intermediate many-one degree between decidable and many-one complete sets as well as further distinctions of reducibility degrees like many-one and truth-table completeness.