Document Open Access Logo

Gödel’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability

Authors Dominik Kirst , Benjamin Peters

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.30.pdf
  • Filesize: 0.71 MB
  • 18 pages

Document Identifiers

Author Details

Dominik Kirst
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany
Benjamin Peters
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany

Cite AsGet BibTex

Dominik Kirst and Benjamin Peters. Gödel’s Theorem Without Tears - Essential Incompleteness in Synthetic Computability. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.30

Abstract

Gödel published his groundbreaking first incompleteness theorem in 1931, stating that a large class of formal logics admits independent sentences which are neither provable nor refutable. This result, in conjunction with his second incompleteness theorem, established the impossibility of concluding Hilbert’s program, which pursued a possible path towards a single formal system unifying all of mathematics. Using a technical trick to refine Gödel’s original proof, the incompleteness result was strengthened further by Rosser in 1936 regarding the conditions imposed on the formal systems. Computability theory, which also originated in the 1930s, was quickly applied to formal logics by Turing, Kleene, and others to yield incompleteness results similar in strength to Gödel’s original theorem, but weaker than Rosser’s refinement. Only much later, Kleene found an improved but far less well-known proof based on computational notions, yielding a result as strong as Rosser’s. In this expository paper, we work in constructive type theory to reformulate Kleene’s incompleteness results abstractly in the setting of synthetic computability theory and assuming a form of Church’s thesis, an axiom internalising the fact that all functions definable in such a setting are computable. Our novel, greatly condensed reformulation showcases the simplicity of the computational argument while staying formally entirely precise, a combination hard to achieve in typical textbook presentations. As an application, we instantiate the abstract result to first-order logic in order to derive essential incompleteness and, along the way, essential undecidability of Robinson arithmetic. This paper is accompanied by a Coq mechanisation covering all our results and based on existing libraries of undecidability proofs and first-order logic, complementing the extensive work on mechanised incompleteness using the Gödel-Rosser approach. In contrast to the related mechanisations, our development follows Kleene’s ideas and utilises Church’s thesis for additional simplicity.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
Keywords
  • incompleteness
  • undecidability
  • synthetic computability theory

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. Lev D. Beklemishev. Gödel incompleteness theorems and the limits of their applicability. i. Russian Mathematical Surveys, 65(5):857, 2010. Google Scholar
  3. Robert S. Boyer, Matt Kaufmann, and J S. Moore. The Boyer-Moore theorem prover and its interactive enhancement. Computers & Mathematics with Applications, 29(2):27-62, 1995. Google Scholar
  4. Alonzo Church. A note on the Entscheidungsproblem. The journal of symbolic logic, 1(1):40-41, 1936. Google Scholar
  5. Thierry Coquand and Gérard Huet. The calculus of constructions. PhD thesis, INRIA, 1986. Google Scholar
  6. Martin Davis, Hilary Putnam, and Julia Robinson. The decision problem for exponential Diophantine equations. Annals of Mathematics, pages 425-436, 1961. Google Scholar
  7. 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
  8. Yannick Forster. Computability in constructive type theory. PhD thesis, Saarland University, 2021. Google Scholar
  9. Yannick Forster. Parametric Church’s thesis: Synthetic computability without choice. In International Symposium on Logical Foundations of Computer Science, pages 70-89. Springer, 2022. Google Scholar
  10. 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, 2019. Google Scholar
  11. 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
  12. 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, 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.
  13. 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.
  14. Torkel Franzén. Gödel’s theorem: an incomplete guide to its use and abuse. AK Peters/CRC Press, 2005. Google Scholar
  15. Kurt Gödel. Über die Vollständigkeit des Logikkalküls. PhD thesis, University of Vienna, 1929. Google Scholar
  16. Kurt Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für mathematik und physik, 38(1):173-198, 1931. Google Scholar
  17. Kurt Gödel. Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik und Physik, 37:349-360, 1930. URL: https://zbmath.org/?q=an%3A56.0046.04.
  18. John Harrison. HOL Light: a tutorial introduction. In Formal Methods in Computer-Aided Design, pages 265-269. Springer Berlin Heidelberg, 1996. Google Scholar
  19. John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009. Google Scholar
  20. Marc Hermes and Dominik Kirst. An analysis of Tennenbaum’s theorem in constructive type theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), 2022. Google Scholar
  21. Douglas R. Hofstadter. Gödel, Escher, Bach. Basic books New York, 1979. Google Scholar
  22. Johannes Hostert, Mark Koch, and Dominik Kirst. A toolbox for mechanised first-order logic. In The Coq Workshop, 2021. Google Scholar
  23. Dominik Kirst and Marc Hermes. Synthetic undecidability and incompleteness of first-order axiom systems in Coq (extended version). To appear. Google Scholar
  24. 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 The Coq Workshop, 2022. Google Scholar
  25. Dominik Kirst and Dominique Larchey-Wendling. Trakhtenbrot’s Theorem in Coq: Finite Model Theory through the Constructive Lens. Logical Methods in Computer Science, Volume 18, Issue 2, June 2022. URL: https://doi.org/10.46298/lmcs-18(2:17)2022.
  26. Stephen C. Kleene. General recursive functions of natural numbers. Mathematische annalen, 112(1):727-742, 1936. Google Scholar
  27. Stephen C. Kleene. Recursive predicates and quantifiers. Transactions of the American Mathematical Society, 53(1):41-73, 1943. Google Scholar
  28. Stephen C. Kleene. A symmetric form of Gödel’s theorem. Journal of Symbolic Logic, 16(2), 1951. Google Scholar
  29. Stephen C. Kleene. Introduction to Metamathematics, 1952. Google Scholar
  30. Stephen C. Kleene. Mathematical Logic. Dover books on mathematics. Dover Publications, 2002. Google Scholar
  31. Georg Kreisel. Church’s thesis: a kind of reducibility axiom for constructive mathematics, 1970. Google Scholar
  32. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq (Extended Version). Logical Methods in Computer Science, Volume 18, Issue 1, March 2022. Google Scholar
  33. Juri V. Matijasevic. Enumerable sets are Diophantine. In Soviet Math. Dokl., volume 11, pages 354-358, 1970. Google Scholar
  34. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283. Springer Science & Business Media, 2002. Google Scholar
  35. Russell O’Connor. Essential incompleteness of arithmetic verified by Coq. In International Conference on Theorem Proving in Higher Order Logics, pages 245-260. Springer, 2005. Google Scholar
  36. 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
  37. 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
  38. 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
  39. Andrei Popescu and Dmitriy Traytel. Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant. Journal of Automated Reasoning, 65(7):1027-1070, 2021. Google Scholar
  40. Emil L. Post. Absolutely unsolvable problems and relatively undecidable propositions-account of an anticipation (1941). Collected Works of Post, pages 375-441, 1994. Google Scholar
  41. Fred Richman. Church’s thesis without tears. The Journal of symbolic logic, 48(3):797-803, 1983. Google Scholar
  42. Barkley Rosser. Extensions of some theorems of Gödel and Church. The journal of symbolic logic, 1(3):87-91, 1936. Google Scholar
  43. Natarajan Shankar. Proof-checking metamathematics. PhD thesis, The University of Texas at Austin, 1986. Google Scholar
  44. Peter Smith. An introduction to Gödel’s theorems. Cambridge University Press, 2013. Google Scholar
  45. Peter Smith. Gödel without (too many) tears, 2021. Google Scholar
  46. Raymond M. Smullyan. Gödel’s incompleteness theorems. Oxford University Press on Demand, 1992. Google Scholar
  47. Andrew W. Swan and Taichi Uemura. On Church’s thesis in cubical assemblies. Mathematical Structures in Computer Science, pages 1-20, 2019. Google Scholar
  48. Stanislaw Swierczkowski. Finite sets and Gödel’s incompleteness theorems. Dissertationes Mathematicae, 422:1-58, 2003. Google Scholar
  49. The Coq Development Team. The Coq proof assistant, January 2022. URL: https://doi.org/10.5281/zenodo.5846982.
  50. Stanley Tennenbaum. Non-Archimedean models for arithmetic. Notices of the American Mathematical Society, 6(270):44, 1959. Google Scholar
  51. Amin Timany and Matthieu Sozeau. Consistency of the predicative calculus of cumulative inductive constructions (pCuIC). CoRR, abs/1710.03912, 2017. URL: http://arxiv.org/abs/1710.03912.
  52. Anne S. Troelstra and Dirk Van Dalen. Constructivism in Mathematics. Vol. 121 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1988. Google Scholar
  53. 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
  54. Benno Van den Berg and Jaap Van Oosten. Arithmetic is categorical, 2011. Technical report. Google Scholar
  55. Norihiro Yamada. Game semantics of Martin-Löf type theory, part III: its consistency with Church’s thesis. arXiv e-prints, 2020. URL: http://arxiv.org/abs/2007.08094.
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