2026-08-12T07:16:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17482 2024-03-06T11:00:05Z ddc:004 open_access

Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq Forster, Yannick Jahn, Felix type theory computability theory constructive mathematics Coq We present a constructive analysis and machine-checked theory of one-one, many-one, and truth-table reductions based on synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying the proof assistant Coq. We give elegant, synthetic, and machine-checked proofs of Post’s landmark results that 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). 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. Proofs can focus on the essence of the argument, without having to sacrifice formality. Synthetic computability also clears the lense for constructivisation. Our constructively careful definition of simple and hypersimple predicates allows us to not assume classical axioms, not even Markov’s principle, still yielding the expected strong results. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yannick Forster and Felix Jahn 2023 Is Part Of LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2023.21 urn:nbn:de:0030-drops-174820 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.21 eng https://creativecommons.org/licenses/by/4.0/legalcode