Niklas Mück: Bachelor's Thesis
The Arithmetical Hierarchy, Oracle Computability, and Post's Theorem in Synthetic Computability
Advisors: Yannick Forster and Dominik Kirst
The subject of this thesis is to formalize the arithmetical hierarchy in constructive type theory, set up synthetic oracle computability including a synthetic definition of the Turing jump,
and connect both by proving Post's theorem in synthetic computability.
We aim at establishing most proofs constructively and mechanize all results in the proof assistant Coq.
Synthetic computability abstracts from concrete models of computation by axiomatically considering all (partial) functions $\mathbb{N}{\to}\mathbb{N}$ as computable which allows to elegantly establish computability theory.
The subject of this thesis is to prove Post's theorem in such a setting.
For that purpose, we formalize two definitions of the arithmetical hierarchy.
The first definition is due to Odifreddi and is explicit in first-order arithmetic without relying on a concrete model of computation.
It classifies formulas in prenex normal form, for which we mechanize a structurally recursive conversion algorithm, via counting the number of quantifier alternations.
The second definition is a synthetic version of the Kleene-Mostowski definition and classifies type-theoretic predicates directly.
After studying the equivalence of the synthetic to the better known first-order definition, based on axioms from synthetic computability, we continue working with the second definition which is more convenient to establish synthetic results with.
As the second main ingredient, we advance a synthetic definition of Turing reductions by Forster and Kirst who follow an idea by Bauer to synthetic oracle machines by adjusting one of its main components, the continuity requirement.
This enables constructive results like the determination of oracle machines solely by a continuous higher-order partial function.
Then, we define a synthetic version of the Turing jump as the halting problem of synthetic oracle machines by assuming an enumerator of continuous higher-order partial functions.
Most of our key results are constructive. Only the final proof of Post's theorem relies on the law of excluded middle whose usage we trace back to exactly two places.
Resources
Submitted thesis: The Arithmetical Hierarchy, Oracle Computability, and Post's Theorem in Synthetic Computability (Coq code) (Coqdoc) (June 18, 2022)
Initial talk: Modeling the arithmetical hierarchy in Coq (January 06, 2022)
Memo: Oracle machines and the Turing jump in synthetic computability (Last updated: March 07, 2022)
Second talk: A Synthetic Definition of the Turing Jump (March 14, 2022)
Final talk: The Arithmetical Hierarchy, Oracle Computability, and Post's Theorem in Synthetic Computability (July 06, 2022)
Legal notice, Privacy policy
