License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2023.21
URN: urn:nbn:de:0030-drops-174820
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17482/
Forster, Yannick ;
Jahn, Felix
Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq
Abstract
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.
BibTeX - Entry
@InProceedings{forster_et_al:LIPIcs.CSL.2023.21,
author = {Forster, Yannick and Jahn, Felix},
title = {{Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {21:1--21:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-264-8},
ISSN = {1868-8969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/17482},
URN = {urn:nbn:de:0030-drops-174820},
doi = {10.4230/LIPIcs.CSL.2023.21},
annote = {Keywords: type theory, computability theory, constructive mathematics, Coq}
}
