Document Open Access Logo

Church’s Thesis and Related Axioms in Coq’s Type Theory

Author Yannick Forster

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.21.pdf
  • Filesize: 0.62 MB
  • 19 pages

Document Identifiers

Author Details

Yannick Forster
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany

Acknowledgements

I want to thank Gert Smolka, Andrej Dudenhefner, Dominik Kirst, and Dominique Larchey-Wendling for discussions and feedback on drafts of this paper. Special thanks go to the anonymous reviewers for their helpful ideas, constructive comments, and editorial suggestions.

Cite AsGet BibTex

Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.21

Abstract

"Church’s thesis" (CT) as an axiom in constructive logic states that every total function of type ℕ → ℕ is computable, i.e. definable in a model of computation. CT is inconsistent both in classical mathematics and in Brouwer’s intuitionism since it contradicts weak Kőnig’s lemma and the fan theorem, respectively. Recently, CT was proved consistent for (univalent) constructive type theory. Since neither weak Kőnig’s lemma nor the fan theorem is a consequence of just logical axioms or just choice-like axioms assumed in constructive logic, it seems likely that CT is inconsistent only with a combination of classical logic and choice axioms. We study consequences of CT and its relation to several classes of axioms in Coq’s type theory, a constructive type theory with a universe of propositions which proves neither classical logical axioms nor strong choice axioms. We thereby provide a partial answer to the question as to which axioms may preserve computational intuitions inherent to type theory, and which certainly do not. The paper can also be read as a broad survey of axioms in type theory, with all results mechanised in the Coq proof assistant.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
Keywords
  • Church’s thesis
  • constructive type theory
  • constructive reverse mathematics
  • synthetic computability theory
  • Coq

Metrics

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

Supplementary Materials

References

  1. Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. Google Scholar
  2. Andrej Bauer. König’s lemma and Kleene tree. unpublished notes, 2006. Google Scholar
  3. Michael J. Beeson. Foundations of constructive mathematics: Metamathematical studies, volume 6. Springer Verlag, 1987. Google Scholar
  4. Josef Berger and Hajime Ishihara. Brouwer’s fan theorem and unique existence in constructive analysis. Mathematical Logic Quarterly, 51(4):360-364, 2005. Google Scholar
  5. Josef Berger, Hajime Ishihara, and Peter Schuster. The weak König lemma, Brouwer’s fan theorem, De Morgan’s law, and dependent choice. Reports on Mathematical Logic, (47):63, 2012. Google Scholar
  6. Yves Bertot and Pierre Castéran. Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, 2013. Google Scholar
  7. Douglas Bridges and Fred Richman. Varieties of constructive mathematics, volume 97. Cambridge University Press, 1987. Google Scholar
  8. T. Coquand. Metamathematical investigations of a calculus of constructions. Technical Report RR-1088, INRIA, September 1989. URL: https://hal.inria.fr/inria-00075471.
  9. Oliver Deiser. A simple continuous bijection from natural sequences to dyadic sequences. The American Mathematical Monthly, 116(7):643-646, 2009. Google Scholar
  10. Radu Diaconescu. Axiom of choice and complementation. Proceedings of the American Mathematical Society, 51(1):176-178, 1975. Google Scholar
  11. Hannes Diener. Constructive Reverse Mathematics. arXiv:1804.05495 [math], April 2020. URL: http://arxiv.org/abs/1804.05495.
  12. Martín H. Escardó and Cory M. Knapp. Partial Elements and Recursion via Dominances in Univalent Type Theory. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.21.
  13. Martín Hötzel Escardó and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  14. 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, pages 38-51, 2019. Google Scholar
  15. Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness theorems for first-order logic analysed in constructive type theory (extended version). arXiv preprint arXiv:2006.04399, 2020. Google Scholar
  16. Yannick Forster and Fabian Kunze. A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17:1-17:19, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.17.
  17. Yannick Forster, Fabian Kunze, and Maximilian Wuttke. Verified programming of Turing machines in Coq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 114-128, 2020. Google Scholar
  18. Yannick Forster and Dominique Larchey-Wendling. Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 104-117, 2019. Google Scholar
  19. Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. A Coq library of undecidable problems. In The Sixth International Workshop on Coq for Programming Languages (CoqPL 2020)., 2020. URL: https://github.com/uds-psl/coq-library-undecidability.
  20. Yannick Forster and Gert Smolka. Weak call-by-value lambda calculus as a model of computation in coq. In International Conference on Interactive Theorem Proving, pages 189-206. Springer, 2017. Google Scholar
  21. Yannick Forster and Gert Smolka. Call-by-value lambda calculus as a model of computation in Coq. Journal of Automated Reasoning, 63(2):393-413, 2019. Google Scholar
  22. Noah Goodman and John Myhill. Choice implies excluded middle. Mathematical Logic Quarterly, 24(25‐30):461-461, 1978. URL: https://doi.org/10.1002/malq.19780242514.
  23. Matt Hendtlass and Robert Lubarsky. Separating fragments of WLEM, LPO, and MP. The Journal of Symbolic Logic, 81(4):1315-1343, December 2016. URL: https://doi.org/10.1017/jsl.2016.38.
  24. Hugo Herbelin. An intuitionistic logic that proves Markov’s principle. In 2010 25th Annual IEEE Symposium on Logic in Computer Science, pages 50-56. IEEE, 2010. Google Scholar
  25. Hajime Ishihara. Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiæ. Travaux d'histoire et de philosophie des sciences, (CS 6):43-59, 2006. Google Scholar
  26. Hajime Ishihara. Weak König’s lemma implies Brouwer’s fan theorem: a direct proof. Notre Dame Journal of Formal Logic, 47(2):249-252, 2006. Google Scholar
  27. Stephen Cole Kleene. On the interpretation of intuitionistic number theory. The journal of symbolic logic, 10(4):109-124, 1945. Google Scholar
  28. Stephen Cole Kleene. Recursive functions and intuitionistic mathematics, 1953. Google Scholar
  29. Georg Kreisel. Church’s thesis: a kind of reducibility axiom for constructive mathematics. In Studies in Logic and the Foundations of Mathematics, volume 60, pages 121-150. 1970. Google Scholar
  30. Dominique Larchey-Wendling. Typing total recursive functions in Coq. In International Conference on Interactive Theorem Proving, pages 371-388. Springer, 2017. Google Scholar
  31. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s tenth problem in Coq. arXiv preprint arXiv:2003.04604, 2020. Google Scholar
  32. Dominique Larchey-Wendling and Jean-François Monin. The Braga method: Extracting certified algorithms from complex recursive schemes in Coq. In Klaus Mainzer, Peter Schuster, and Helmut Schwichtenberg, editors, Proof and Computation: From Proof Theory and Univalent Mathematics to Program Extraction and Verification. World Scientific Singapore, 2021. Google Scholar
  33. Pierre Letouzey. Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. PhD thesis, L’Université de Paris-Sud, July 2004. URL: http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.pdf.
  34. Andrei Andreevich Markov. The theory of algorithms. Trudy Matematicheskogo Instituta Imeni VA Steklova, 42:3-375, 1954. Google Scholar
  35. 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. Google Scholar
  36. Pierre-Marie Pédrot and Nicolas Tabareau. Failure is not an option. In European Symposium on Programming, pages 245-271. Springer, 2018. Google Scholar
  37. Fred Richman. Church’s thesis without tears. The Journal of symbolic logic, 48(3):797-803, 1983. Google Scholar
  38. Fred Richman. The fundamental theorem of algebra: a constructive development without choice. Pacific Journal of Mathematics, 196(1):213-230, 2000. Google Scholar
  39. Fred Richman. Constructive Mathematics without Choice. In Peter Schuster, Ulrich Berger, and Horst Osswald, editors, Reuniting the Antipodes emdash Constructive and Nonstandard Views of the Continuum, pages 199-205. Springer Netherlands, Dordrecht, 2001. URL: https://doi.org/10.1007/978-94-015-9757-9_17.
  40. Helmut Schwichtenberg. A direct proof of the equivalence between Brouwer’s fan theorem and König’s lemma with a uniqueness hypothesis. J. UCS, 11(12):2086-2095, 2005. Google Scholar
  41. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The MetaCoq Project. Journal of Automated Reasoning, February 2020. URL: https://doi.org/10.1007/s10817-019-09540-0.
  42. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proceedings of the ACM on Programming Languages, 4(POPL):1-28, 2019. Google Scholar
  43. Andrew Swan and Taichi Uemura. On Church’s thesis in cubical assemblies. arXiv preprint arXiv:1905.03014, 2019. Google Scholar
  44. The Coq Development Team. The Coq Proof Assistant, version 8.11.0. https://doi.org/10.5281/zenodo.3744225, jan 2020.
  45. The Coq std++ Team. An extended "standard library" for Coq. https://gitlab.mpi-sws.org/iris/stdpp, 2020.
  46. Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in mathematics. vol. i, volume 121 of. Studies in Logic and the Foundations of Mathematics, 26, 1988. Google Scholar
  47. Benjamin Werner. Sets in types, types in sets. In International Symposium on Theoretical Aspects of Computer Software, pages 530-546. Springer, 1997. Google Scholar
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