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. As a prerequiste we discuss underlying concepts like limit computability due to Shoenfield and Gold and their definition in synthetic computability.
Goals
We aim to show that the following theorem and construction in synthetic computability.
- Limit Lemma
- Low Simple Set
- Friedberg–Muchnik Theorem
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 [Ongoing]
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
Legal notice, Privacy policy
