Niklas Mück: Bachelor's Thesis
The Arithmetical Hierarchy and Post’s Theorem in Coq
Advisors: Yannick Forster and Dominik Kirst
It is well-known that the halting problem is undecidable, and that there are
harder problems that still cannot be decided even when extending the model of
computation with an oracle for the halting problem.
Post's theorem connects two of these hierarchies, namely Turing jumps and the arithmetical hierarchy.
In order to study the relative computability of decision problems, Turing came
up with the idea of oracle machines - Turing machines with an additional operation
for querying a black-box solver for a given problem.
Having such a model of computation, one can define the Turing jump of a set $Q$ as
the halting problem of oracle machines with an oracle for $Q$. The Turing
jump of $Q$ is not decidable by an oracle machine with an oracle for $Q$.
This gives rise to a hierarchy of unsolvability.
The arithmetical hierarchy classifies sets of numbers according to the syntactical
complexity of the first-order formula in Peano arithmetic that defines them.
In prenex normal form (i.e. all quantifiers in front) the number of quantifier
alternations gives the degree of unsolvability.
I'm currently working on:
- Constructing a prenex normal form conversion of first order formulas in Coq
- Modeling different definitions of the arithmetical hierarchy in Coq
- one in a concrete model of computation i.e. Peano Arithmetic
- the other one lifted to meta-theory
- A synthetic definition of oracle machines and the Turing jump
- Proving Post's theorem in synthetic computability using Coq
Initial talk: Modeling the arithmetical hierarchy in Coq (January 06, 2022)
Memo: Oracle machines and the Turing jump in synthetic computability (Last updated: March 7, 2022)
Second talk: A Synthetic Definition of the Turing Jump (March 14, 2022)