Haoyi Zeng: Bachelor's Thesis
Post's problem and the priority method
Advisors: Yannick Forster and Dominik Kirst
Summary
We explore giving a solution to Post's Problem in synthetic computability. In 1944, Post posed the question whether there is a semi-decidable yet undecidable predicate that is simpler than the Halting Problem w.r.t. Turing reducibility, i.e. such that the halting problem does not reduce to the predicate. The question was answered independently in 1956/57 by Friedberg and Muchnik using the so-called "priority method". To formalise a solution in synthetic computability, we focus on capturing the priority method synthetically in order to use it for a construction due to Soare (1980), which is simpler than the Friedberg/Muchnik construction. With this approach, we formalise the construction of the low simple predicate in constructive type theory and mechanise our results in the Coq proof assistant.
Goals
We aim to show that the following theorem and construction in synthetic computability.
- Limit Lemma
- Low Simple Set
Current state
A memo outlining the current state can be found below. As an overview, we formalize the following results or works in progress.
- Limit Lemma
- Low Simple Set
References
Resources
A memo on the current state can be found here.
First seminar talk:
Post's Problem and The Priority Method in Synthetic Computability
Second seminar talk:
Post's Problem and The Priority Method in Synthetic Computability
Legal notice, Privacy policy
