Document Open Access Logo

Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq

Authors Dominik Kirst , Marc Hermes

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.23.pdf
  • Filesize: 0.76 MB
  • 20 pages

Document Identifiers

Author Details

Dominik Kirst
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany
Marc Hermes
  • Universität des Saarlandes, Department of Mathematics, Saarbrücken, Germany

Acknowledgements

The authors want to thank Andrej Dudenhefner, Yannick Forster, Lennard Gäher, Julian Rosemann, Gert Smolka, and the anonymous reviewers for helpful comments and suggestions on earlier drafts of this paper.

Cite AsGet BibTex

Dominik Kirst and Marc Hermes. Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.23

Abstract

We mechanise the undecidability of various first-order axiom systems in Coq, employing the synthetic approach to computability underlying the growing Coq Library of Undecidability Proofs. Concretely, we cover both semantic and deductive entailment in fragments of Peano arithmetic (PA) and Zermelo-Fraenkel set theory (ZF), with their undecidability established by many-one reductions from solvability of Diophantine equations, i.e. Hilbert’s tenth problem (H10), and the Post correspondence problem (PCP), respectively. In the synthetic setting based on the computability of all functions definable in a constructive foundation, such as Coq’s type theory, it suffices to define these reductions as meta-level functions with no need for further encoding in a formalised model of computation. The concrete cases of PA and ZF are prepared by a general synthetic theory of undecidable axiomatisations, focusing on well-known connections to consistency and incompleteness. Specifically, our reductions rely on the existence of standard models, necessitating additional assumptions in the case of full ZF, and all axiomatic extensions still justified by such standard models are shown incomplete. As a by-product of the undecidability of ZF formulated using only membership and no equality symbol, we obtain the undecidability of first-order logic with a single binary relation.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
Keywords
  • undecidability
  • synthetic computability
  • first-order logic
  • incompleteness
  • Peano arithmetic
  • ZF set theory
  • constructive type theory
  • Coq

Metrics

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

Supplementary Materials

References

  1. Peter Aczel. The type theoretic interpretation of constructive set theory. In Studies in Logic and the Foundations of Mathematics, volume 96, pages 55-66. Elsevier, 1978. Google Scholar
  2. Bruno Barras. Sets in Coq, Coq in sets. Journal of Formalized Reasoning, 3(1):29-48, 2010. Google Scholar
  3. Andrej Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. Google Scholar
  4. Thomas Braibant and Damien Pous. An efficient Coq tactic for deciding Kleene algebras. In International Conference on Interactive Theorem Proving, pages 163-178. Springer, 2010. Google Scholar
  5. Alan Bundy, Fausto Giunchiglia, Adolfo Villafiorita, and Toby Walsh. An incompleteness theorem via abstraction, 1996. Technical report. Google Scholar
  6. Alonzo Church et al. A note on the Entscheidungsproblem. J. Symb. Log., 1(1):40-41, 1936. Google Scholar
  7. Nicolaas G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. Google Scholar
  8. John Doner and Wilfrid Hodges. Alfred Tarski and decidable theories. The Journal of symbolic logic, 53(1):20-35, 1988. Google Scholar
  9. 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 LIPIcs, pages 21:1-21:19, Dagstuhl, Germany, 2021. Google Scholar
  10. Yannick Forster, Edith Heiter, and Gert Smolka. Verification of PCP-related computational reductions in Coq. In International Conference on Interactive Theorem Proving, pages 253-269. Springer, 2018. Google Scholar
  11. 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
  12. Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness theorems for first-order logic analysed in constructive type theory: Extended version. Journal of Logic and Computation, 31(1):112-151, 2021. Google Scholar
  13. 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 LIPIcs, pages 17:1-17:19, Dagstuhl, Germany, 2019. Google Scholar
  14. 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 CoqPL 2020, New Orleans, LA, United States, 2020. URL: https://github.com/uds-psl/coq-library-undecidability.
  15. Jesse Han and Floris van Doorn. A formal proof of the independence of the continuum hypothesis. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 353-366, 2020. Google Scholar
  16. David Hilbert and Wilhelm Ackermann. Grundzüge der theoretischen Logik. Springer, 1928. Google Scholar
  17. Dominik Kirst and Dominique Larchey-Wendling. Trakhtenbrot’s theorem in Coq: a constructive approach to finite model theory. In International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, Paris, France, 2020. Springer. Google Scholar
  18. Dominik Kirst and Gert Smolka. Large model constructions for second-order ZF in dependent type theory. Certified Programs and Proofs - 7th International Conference, CPP 2018, Los Angeles, USA, 2018, January 2018. Google Scholar
  19. 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. Elsevier, 1970. Google Scholar
  20. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s tenth problem in Coq. In 4th International Conference on Formal Structures for Computation and Deduction, volume 131 of LIPIcs, pages 27:1-27:20, February 2019. Google Scholar
  21. Olivier Laurent. An anti-locally-nameless approach to formalizing quantifiers. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 300-312, 2021. Google Scholar
  22. Petar Maksimović and Alan Schmitt. HOCore in Coq. In International Conference on Interactive Theorem Proving, pages 278-293. Springer, 2015. Google Scholar
  23. John Myhill. Some properties of intuitionistic Zermelo-Frankel set theory. In Cambridge Summer School in Mathematical Logic, pages 206-231. Springer, 1973. Google Scholar
  24. Russell O'Connor. Essential incompleteness of arithmetic verified by Coq. In Joe Hurd and Tom Melham, editors, Theorem Proving in Higher Order Logics, pages 245-260, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  25. Lawrence C. Paulson. A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. Journal of Automated Reasoning, 55(1):1-37, 2015. Google Scholar
  26. Andrei Popescu and Dmitriy Traytel. A formally verified abstract account of Gödel’s incompleteness theorems. In International Conference on Automated Deduction, pages 442-461. Springer, 2019. Google Scholar
  27. Emil L. Post. Recursively enumerable sets of positive integers and their decision problems. bulletin of the American Mathematical Society, 50(5):284-316, 1944. Google Scholar
  28. Mojżesz Presburger and Dale Jabcquette. On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation. History and Philosophy of Logic, 12(2):225-233, 1991. Google Scholar
  29. Art Quaife. Automated proofs of Löb’s theorem and Gödel’s two incompleteness theorems. Journal of Automated Reasoning, 4(2):219-231, 1988. Google Scholar
  30. Fred Richman. Church’s thesis without tears. The Journal of symbolic logic, 48(3):797-803, 1983. Google Scholar
  31. Steven Schäfer, Gert Smolka, and Tobias Tebbi. Completeness and decidability of de Bruijn substitution algebra in Coq. In Proceedings of the 2015 Conference on Certified Programs and Proofs, pages 67-73. ACM, 2015. Google Scholar
  32. Natarajan Shankar. Proof-checking metamathematics. The University of Texas at Austin, 1986. PhD Thesis. Google Scholar
  33. Wilfried Sieg and Clinton Field. Automated search for Gödel’s proofs. In Deduction, Computation, Experiment, pages 117-140. Springer, 2008. Google Scholar
  34. Gert Smolka and Kathrin Stark. Hereditarily finite sets in constructive type theory. In Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-27, 2016, volume 9807 of LNCS, pages 374-390. Springer, 2016. Google Scholar
  35. Raymond M. Smullyan and Melvin Fitting. Set theory and the continuum problem. Dover Publications, 2010. Google Scholar
  36. 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, 2020. Google Scholar
  37. Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In International Conference on Certified Programs and Proofs, pages 166-180. ACM, 2019. Google Scholar
  38. The Coq Development Team. The Coq Proof Assistant, version 8.12.0, 2020. URL: https://doi.org/10.5281/zenodo.4021912.
  39. Stanley Tennenbaum. Non-Archimedean models for arithmetic. Notices of the American Mathematical Society, 6(270):44, 1959. Google Scholar
  40. Boris A. Trakhtenbrot. The impossibility of an algorithm for the decidability problem on finite classes. Dokl. Akad. Nok. SSSR, 70(4):569-572, 1950. Google Scholar
  41. Alan M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London mathematical society, 2(1):230-265, 1937. Google Scholar
  42. Benjamin Werner. Sets in types, types in sets. In Theoretical Aspects of Computer Software, pages 530-546. Springer, Berlin, Heidelberg, 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