A Constructive and Synthetic Theory of Reducibility: Myhill's Isomorphism Theorem and Post's Problem for Many-one and Truth-table Reducibility in Coq (Full Version)

We present a constructive analysis and machine-checked synthetic approach to the theory of one-one, many-one, and truth-table reductions carried out in the Calculus of Inductive Constructions, the type theory underlying the proof assistant Coq. In synthetic computability, one assumes axioms allowing to carry out computability theory with all definitions and proofs purely in terms of functions of the type theory with no mention of a model of computation. Our synthetic proof of Myhill's isomorphism theorem that one-one equivalence yields a computational isomorphism makes a compelling case for synthetic computability due to its simplicity without sacrificing formality. Synthetic computability also clears the lense for constructivisation. We do not assume classical axioms, not even Markov's principle, possible by a careful constructivised definition of simple and hypersimple predicates, still yielding the expected strong results: a simple predicate exists, is enumerable, undecidable, but many-one incomplete (Post's problem for many-one reducibility), and a hypersimple predicate exists, is enumerable, undecidable, but truth-table incomplete (Post's problem for truth-table reducibility)