# 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

## Resources

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)