Document Open Access Logo

The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions

Authors Yannick Forster , Dominik Kirst , Niklas Mück

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.29.pdf
  • Filesize: 0.88 MB
  • 20 pages

Document Identifiers

Author Details

Yannick Forster
  • Inria, Nantes Université, LS2N, Nantes, France
Dominik Kirst
  • Ben-Gurion University of the Negev, Beer-Sheva, Israel
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
Niklas Mück
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
  • MPI-SWS, Saarland Informatics Campus, Saarbrücken, Germany

Funding

  • Forster, Yannick: received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 101024493.
  • Kirst, Dominik: is supported by a Minerva Fellowship of the Minerva Stiftung Gesellschaft für die Forschung mbH.

Acknowledgements

We want to thank Felix Jahn, Gert Smolka, Dominique Larchey-Wendling, and the participants of the TYPES '22 conference for many fruitful discussions about Turing reducibility, Ian Shillito and the anonymous reviewers of this paper for helpful feedback, as well as Martin Baillon, Yann Leray, Assia Mahboubi, Pierre-Marie Pédrot, and Matthieu Piquerez for discussions about notions of continuity. The central inspiration to start working on Turing reducibility in type theory is due to Andrej Bauer’s talk at the Wisconsin logic seminar in February 2021. Furthermore, the first two authors want to thank Benjamin Kaminski, his research group, and the royals of the castle for hosting their nostalgic stay in Saarbrücken to finish writing this paper.

Cite AsGet BibTex

Yannick Forster, Dominik Kirst, and Niklas Mück. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.29

Abstract

The Kleene-Post theorem and Post’s theorem are two central and historically important results in the development of oracle computability theory, clarifying the structure of Turing reducibility degrees. They state, respectively, that there are incomparable Turing degrees and that the arithmetical hierarchy is connected to the relativised form of the halting problem defined via Turing jumps. We study these two results in the calculus of inductive constructions (CIC), the constructive type theory underlying the Coq proof assistant. CIC constitutes an ideal foundation for the formalisation of computability theory for two reasons: First, like in other constructive foundations, computable functions can be treated via axioms as a purely synthetic notion rather than being defined in terms of a concrete analytic model of computation such as Turing machines. Furthermore and uniquely, CIC allows consistently assuming classical logic via the law of excluded middle or weaker variants on top of axioms for synthetic computability, enabling both fully classical developments and taking the perspective of constructive reverse mathematics on computability theory. In the present paper, we give a fully constructive construction of two Turing-incomparable degrees à la Kleene-Post and observe that the classical content of Post’s theorem seems to be related to the arithmetical hierarchy of the law of excluded middle due to Akama et. al. Technically, we base our investigation on a previously studied notion of synthetic oracle computability and contribute the first consistency proof of a suitable enumeration axiom. All results discussed in the paper are mechanised and contributed to the Coq library of synthetic computability.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
Keywords
  • Constructive mathematics
  • Computability theory
  • Logical foundations
  • Constructive type theory
  • Interactive theorem proving
  • Coq proof assistant

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Yohji Akama, Stefano Berardi, Susumu Hayashi, and Ulrich Kohlenbach. An arithmetical hierarchy of the law of excluded middle and related principles. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 192-201. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319613.
  2. Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. URL: https://doi.org/10.1016/j.entcs.2005.11.049.
  3. Andrej Bauer. On fixed-point theorems in synthetic computability. Tbilisi Mathematical Journal, 10(3):167-181, 2017. URL: https://doi.org/10.1515/tmj-2017-0107.
  4. Andrej Bauer. Synthetic mathematics with an excursion into computability theory (slide set). University of Wisconsin Logic seminar, 2020. URL: http://math.andrej.com/asset/data/madison-synthetic-computability-talk.pdf.
  5. Vasco Brattka, Matthew Hendtlass, and Alexander P. Kreuzer. On the uniform computational content of computability theory. Theory of Computing Systems, 61(4):1376-1426, August 2017. URL: https://doi.org/10.1007/s00224-017-9798-1.
  6. S Barry Cooper. Computability theory. CRC Press, 2003. URL: https://doi.org/10.1201/9781315275789.
  7. Thierry Coquand. Metamathematical investigations of a calculus of constructions. Technical Report RR-1088, INRIA, 1989. URL: https://hal.inria.fr/inria-00075471.
  8. Thierry Coquand and Gérard P Huet. The calculus of constructions. Information and Computation, 76(2/3):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  9. Hannes Diener. Constructive Reverse Mathematics. arXiv:1804.05495 [math], 2020. URL: https://arxiv.org/abs/1804.05495.
  10. Hannes Diener and Hajime Ishihara. Bishop-style constructive reverse mathematics. In Theory and Applications of Computability, pages 347-365. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-59234-9_10.
  11. Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.21.
  12. Yannick Forster. Computability in Constructive Type Theory. PhD thesis, Saarland University, 2021. URL: https://doi.org/10.22028/D291-35758.
  13. Yannick Forster. Parametric Church’s Thesis: Synthetic computability without choice. In International Symposium on Logical Foundations of Computer Science, pages 70-89. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-93100-1_6.
  14. Yannick Forster and Felix Jahn. Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:21, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.21.
  15. Yannick Forster, Dominik Kirst, and Niklas Mück. Oracle computability and turing reducibility in the calculus of inductive constructions, 2023. URL: https://arxiv.org/abs/2307.15543.
  16. Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2019. ACM Press, 2019. URL: https://doi.org/10.1145/3293880.3294091.
  17. Yannick Forster, Fabian Kunze, and Nils Lauermann. Synthetic Kolmogorov Complexity in Coq. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1-12:19, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.12.
  18. R. M. Friedberg. Two recursively enumerable sets of incomparable degrees of unsovlability (solution of Post’s problem), 1944. Proceedings of the National Academy of Sciences, 43(2):236-238, February 1957. URL: https://doi.org/10.1073/pnas.43.2.236.
  19. Makoto Fujiwara and Taishi Kurahashi. Prenex normal form theorems in semi-classical arithmetic. The Journal of Symbolic Logic, 86(3):1124-1153, 2021. URL: https://doi.org/10.1017/jsl.2021.47.
  20. Makoto Fujiwara and Taishi Kurahashi. Prenex normalization and the hierarchical classification of formulas, 2023. URL: https://arxiv.org/abs/2302.11808.
  21. Matt Hendtlass and Robert Lubarsky. Separating fragments of WLEM, LPO, and MP. The Journal of Symbolic Logic, 81(4):1315-1343, 2016. URL: https://doi.org/10.1017/jsl.2016.38.
  22. Marc Hermes and Dominik Kirst. An analysis of Tennenbaum’s theorem in constructive type theory. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel, volume 228 of LIPIcs, pages 9:1-9:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.9.
  23. J. Martin E. Hyland. The effective topos. In The L. E. J. Brouwer Centenary Symposium, Proceedings of the Conference held in Noordwijkerhout, pages 165-216. Elsevier, 1982. URL: https://doi.org/10.1016/s0049-237x(09)70129-6.
  24. Hajime Ishihara. Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientae, CS 6:43-59, September 2006. URL: https://doi.org/10.4000/philosophiascientiae.406.
  25. Dominik Kirst. Mechanised Metamathematics: An Investigation of First-Order Logic and Set Theory in Constructive Type Theory. PhD thesis, Saarland University, 2022. URL: https://doi.org/10.22028/D291-39150.
  26. Dominik Kirst, Yannick Forster, and Niklas Mück. Synthetic Versions of the Kleene-Post and Post’s Theorem. 28th International Conference on Types for Proofs and Programs (TYPES 2022), 2022. URL: https://types22.inria.fr/files/2022/06/TYPES_2022_paper_65.pdf.
  27. Dominik Kirst, Johannes Hostert, Andrej Dudenhefner, Yannick Forster, Marc Hermes, Mark Koch, Dominique Larchey-Wendling, Niklas Mück, Benjamin Peters, Gert Smolka, and Dominik Wehr. A Coq library for mechanised first-order logic. In Coq Workshop, 2022. URL: https://coq-workshop.gitlab.io/2022/abstracts/Coq2022-01-01-first-order-logic.pdf.
  28. Dominik Kirst and Benjamin Peters. Gödel’s theorem without tears - Essential incompleteness in synthetic computability. In Bartek Klin and Elaine Pimentel, editors, 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, volume 252 of LIPIcs, pages 30:1-30:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.30.
  29. S. C. Kleene. Countable functionals. Journal of Symbolic Logic, 27(3):81-100, 1959. URL: https://doi.org/10.2307/2964658.
  30. Stephen C. Kleene. Recursive predicates and quantifiers. Transactions of the American Mathematical Society, 53(1):41-73, 1943. URL: https://doi.org/10.1090/S0002-9947-1943-0007371-8.
  31. Steven C. Kleene and Emil L. Post. The upper semi-lattice of degrees of recursive unsolvability. The Annals of Mathematics, 59(3):379, May 1954. URL: https://doi.org/10.2307/1969708.
  32. Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pages 101-128. North-Holland Pub. Co., 1959. Google Scholar
  33. Georg Kreisel. Mathematical logic. Lectures in modern mathematics, 3:95-195, 1965. URL: https://doi.org/10.2307/2315573.
  34. Andrei A. Markov. The theory of algorithms. Trudy Matematicheskogo Instituta Imeni VA Steklova, 42:3-375, 1954. URL: https://doi.org/10.1007/978-94-017-3477-6.
  35. Andrzej Mostowski. On definable sets of positive integers. Fundamenta Mathematicae, 34:81-112, 1947. URL: https://doi.org/10.4064/fm-34-1-81-112.
  36. Albert Abramovich Muchnik. On strong and weak reducibility of algorithmic problems. Sibirskii Matematicheskii Zhurnal, 4(6):1328-1341, 1963. Google Scholar
  37. Niklas Mück. The Arithmetical Hierarchy, Oracle Computability, and Post’s Theorem in Synthetic Computability. Bachelor’s thesis, Saarland University, 2022. URL: https://ps.uni-saarland.de/~mueck/bachelor.php.
  38. Piergiorgio Odifreddi. Classical recursion theory: The theory of functions and sets of natural numbers. Elsevier, 1992. Google Scholar
  39. Christine Paulin-Mohring. Inductive definitions in the system Coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, pages 328-345. Springer, 1993. URL: https://doi.org/10.1007/BFb0037116.
  40. Emil L. Post. Recursively enumerable sets of positive integers and their decision problems. bulletin of the American Mathematical Society, 50(5):284-316, 1944. URL: https://doi.org/10.1090/S0002-9904-1944-08111-1.
  41. Emil L. Post. Degrees of recursive unsolvability - Preliminary report. In Bulletin of the American Mathematical Society, volume 54:7, pages 641-642. American Mathematical Society (AMS), 1948. Google Scholar
  42. Fred Richman. Church’s thesis without tears. The Journal of symbolic logic, 48(3):797-803, 1983. URL: https://doi.org/10.2307/2273473.
  43. Hartley Rogers. Theory of Recursive Functions and Effective Computability. MIT Press, Cambridge, MA, USA, 1987. Google Scholar
  44. Sam Sanders. Refining the taming of the reverse mathematics zoo. Notre Dame Journal of Formal Logic, 59(4), January 2018. URL: https://doi.org/10.1215/00294527-2018-0015.
  45. Robert I. Soare. Recursively enumerable sets and degrees: A study of computable functions and computably generated sets. Springer Science & Business Media, 1999. Google Scholar
  46. Andrew Swan and Taichi Uemura. On Church’s thesis in cubical assemblies. arXiv preprint, 2019. URL: https://arxiv.org/abs/1905.03014.
  47. Andrew W Swan. Oracle modalities. Second International Conference on Homotopy Type Theory (HoTT 2023), 2023. URL: https://hott.github.io/HoTT-2023/abstracts/HoTT-2023_abstract_35.pdf.
  48. The Coq Development Team. The Coq proof assistant, June 2023. URL: https://doi.org/10.5281/zenodo.8161141.
  49. Jaap van Oosten. Partial combinatory algebras of functions. Notre Dame Journal of Formal Logic, 52(4):431-448, 2011. URL: https://doi.org/10.1215/00294527-1499381.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact