Haoyi Zeng: Bachelor's Thesis

Saarland University Computer Science

Post's problem and the priority method

Advisors: Yannick Forster and Dominik Kirst


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.


We aim to show that the following theorem and construction in synthetic computability.

Current state

A memo outlining the current state can be found below. As an overview, we formalize the following results or works in progress.



  • 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