# 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