# 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