Document Open Access Logo

A Succinct Formalization of the Completeness of First-Order Logic

Author Asta Halkjær From

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2021.8.pdf
  • Filesize: 0.75 MB
  • 24 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • First-Order Logic
  • Completeness
  • Isabelle/HOL

Metrics

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

Abstract

I succinctly formalize the soundness and completeness of a small Hilbert system for first-order logic in the proof assistant Isabelle/HOL. The proof combines and details ideas from de Bruijn, Henkin, Herbrand, Hilbert, Hintikka, Lindenbaum, Smullyan and others in a novel way, and I use a declarative style, custom notation and proof automation to obtain a readable formalization. The formalized definitions of Hintikka sets and Herbrand structures allow open and closed formulas to be treated uniformly, making free variables a non-concern. This paper collects important techniques in mathematical logic in a way suited for both study and further work.

Cite As Get BibTex

Asta Halkjær From. A Succinct Formalization of the Completeness of First-Order Logic. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.TYPES.2021.8

Author Details

Asta Halkjær From
  • Technical University of Denmark, Kongens Lyngby, Denmark

Acknowledgements

Thanks to Frederik Krogsdal Jacobsen, Alexander Birch Jensen and Jørgen Villadsen for their useful comments. I am especially grateful to the anonymous reviewers for their insightful remarks which have improved both the formalization and the paper.

Supplementary Materials

References

  1. Jon Barwise. An introduction to first-order logic. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 5-46. Elsevier, 1977. URL: https://doi.org/10.1016/S0049-237X(08)71097-8.
  2. Bruno Bentzen. A Henkin-style completeness proof for the modal logic S5. In Pietro Baroni, Christoph Benzmüller, and Yì N. Wáng, editors, Logic and Argumentation - 4th International Conference, CLAR 2021, Hangzhou, China, October 20-22, 2021, Proceedings, volume 13040 of Lecture Notes in Computer Science, pages 459-467. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-89391-0_25.
  3. Stefan Berghofer. First-order logic according to Fitting. Archive of Formal Proofs, August 2007. Formal proof development. URL: https://isa-afp.org/entries/FOL-Fitting.html.
  4. Jasmin Christian Blanchette. Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pages 1-13. ACM, 2019. Google Scholar
  5. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Abstract completeness. Archive of Formal Proofs, April 2014. Formal proof development. URL: https://isa-afp.org/entries/Abstract_Completeness.html.
  6. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning, 58(1):149-179, 2017. URL: https://doi.org/10.1007/s10817-016-9391-3.
  7. Patrick Braselmann and Peter Koepke. Gödel’s completeness theorem. Formalized Mathematics, 13(1):49-53, 2005. Google Scholar
  8. Robert L. Constable and Mark Bickford. Intuitionistic completeness of first-order logic. Annals of Pure and Applied Logic, 165(1):164-198, 2014. URL: https://doi.org/10.1016/j.apal.2013.07.009.
  9. N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer, editors, Selected Papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics, pages 375-388. Elsevier, 1994. Reprinted from: Indagationes Math, 34, 5, p. 381-392, by courtesy of the Koninklijke Nederlandse Akademie van Wetenschappen, Amsterdam. URL: https://doi.org/10.1016/S0049-237X(08)70216-7.
  10. Melvin Fitting. First-Order Logic and Automated Theorem Proving, Second Edition. Graduate Texts in Computer Science. Springer, 1996. Google Scholar
  11. Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness theorems for first-order logic analysed in constructive type theory. Journal of Logic and Computation, 31(1):112-151, 2021. URL: https://doi.org/10.1093/logcom/exaa073.
  12. Asta Halkjær From. Synthetic completeness for a terminating Seligman-style tableau system. In Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch, editors, 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy, volume 188 of LIPIcs, pages 5:1-5:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.TYPES.2020.5.
  13. Asta Halkjær From. Formalizing Henkin-style completeness of an axiomatic system for propositional logic. In WESSLLI + ESSLLI Virtual Student Session, 2021. Accepted for post-proceedings. Google Scholar
  14. Asta Halkjær From, Anders Schlichtkrull, and Jørgen Villadsen. A sequent calculus for first-order logic formalized in Isabelle/HOL. In Stefania Monica and Federico Bergenti, editors, Proceedings of the 36th Italian Conference on Computational Logic, Parma, Italy, September 7-9, 2021, volume 3002 of CEUR Workshop Proceedings, pages 107-121. CEUR-WS.org, 2021. URL: http://ceur-ws.org/Vol-3002/paper7.pdf.
  15. Asta Halkjær From. Formalizing a Seligman-style tableau system for hybrid logic. Archive of Formal Proofs, December 2019. Formal proof development. URL: http://isa-afp.org/entries/Hybrid_Logic.html.
  16. Asta Halkjær From. A sequent calculus for first-order logic. Archive of Formal Proofs, July 2019. Formal proof development. URL: https://isa-afp.org/entries/FOL_Seq_Calc1.html.
  17. Asta Halkjær From. Soundness and completeness of an axiomatic system for first-order logic. Archive of Formal Proofs, September 2021. Formal proof development. URL: https://isa-afp.org/entries/FOL_Axiomatic.html.
  18. Herman Geuvers. Proof assistants: History, ideas and future. Sadhana, 34(1):3-25, 2009. URL: https://doi.org/10.1007/s12046-009-0001-5.
  19. Kurt Gödel. Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik und Physik, 37(1):349-360, 1930. Google Scholar
  20. John Harrison. Formalizing basic first order model theory. In Jim Grundy and Malcolm C. Newey, editors, Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, volume 1479 of Lecture Notes in Computer Science, pages 153-170. Springer, 1998. URL: https://doi.org/10.1007/BFb0055135.
  21. Leon Henkin. The discovery of my completeness proofs. Bulletin of Symbolic Logic, 2(2):127-158, 1996. URL: https://doi.org/10.2307/421107.
  22. Hugo Herbelin and Danko Ilik. An analysis of the constructive content of Henkin’s proof of Gödel’s completeness theorem. Manuscript available online, 2016. Google Scholar
  23. Jacques Herbrand. Recherches sur la théorie de la démonstration. Number 110 in Thèses de l'entre-deux-guerres. Faculté des Sciences de L'Université de Paris, 1930. Google Scholar
  24. Denis R. Hirschfeldt. Slicing the Truth - On the Computable and Reverse Mathematics of Combinatorial Principles, volume 28 of Lecture Notes Series / Institute for Mathematical Sciences / National University of Singapore. World Scientific, 2014. URL: https://doi.org/10.1142/9208.
  25. Danko Ilik. Constructive Completeness Proofs and Delimited Control. (Preuves constructives de complétude et contrôle délimité). PhD thesis, École Polytechnique, Palaiseau, France, 2010. URL: https://tel.archives-ouvertes.fr/tel-00529021.
  26. Klaus Frovin Jørgensen, Patrick Blackburn, Thomas Bolander, and Torben Braüner. Synthetic completeness proofs for Seligman-style tableau systems. In Lev D. Beklemishev, Stéphane Demri, and András Maté, editors, Advances in Modal Logic 11, proceedings of the 11th conference on "Advances in Modal Logic," held in Budapest, Hungary, August 30 - September 2, 2016, pages 302-321. College Publications, 2016. URL: http://www.aiml.net/volumes/volume11/Joergensen-Blackburn-Bolander-Brauner.pdf.
  27. Olivier Laurent. An anti-locally-nameless approach to formalizing quantifiers. In Catalin Hritcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 300-312. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439926.
  28. Pierre Lescanne. From lambda-sigma to lambda-upsilon: a journey through calculi of explicit substitutions. In Hans-Juergen Boehm, Bernard Lang, and Daniel M. Yellin, editors, Conference Record of POPL'94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994, pages 60-69. ACM Press, 1994. URL: https://doi.org/10.1145/174675.174707.
  29. James Margetson and Tom Ridge. Completeness theorem. Archive of Formal Proofs, September 2004. Formal proof development. URL: http://isa-afp.org/entries/Completeness.html.
  30. Julius Michaelis and Tobias Nipkow. Propositional proof systems. Archive of Formal Proofs, June 2017. Formal proof development. URL: http://isa-afp.org/entries/Propositional_Proof_Systems.html.
  31. Julius Michaelis and Tobias Nipkow. Formalized Proof Systems for Propositional Logic. In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, editors, 23rd International Conference on Types for Proofs and Programs (TYPES 2017), volume 104 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2017.5.
  32. Tobias Nipkow. More Church-Rosser proofs. Journal of Automated Reasoning, 26(1):51-66, 2001. URL: https://doi.org/10.1023/A:1006496715975.
  33. Tobias Nipkow and Gerwin Klein. Concrete Semantics - With Isabelle/HOL. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10542-0.
  34. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  35. Henrik Persson. Constructive completeness of intuitionistic predicate logic. Licenciate thesis, Chalmers University of Technology, 1996. Google Scholar
  36. Andrei Popescu and Dmitriy Traytel. A formally verified abstract account of Gödel’s incompleteness theorems. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, volume 11716 of Lecture Notes in Computer Science, pages 442-461. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29436-6_26.
  37. Anders Schlichtkrull. The resolution calculus for first-order logic. Archive of Formal Proofs, June 2016. Formal proof development. URL: http://isa-afp.org/entries/Resolution_FOL.html.
  38. Anders Schlichtkrull. Formalization of the resolution calculus for first-order logic. Journal of Automated Reasoning, 61(1-4):455-484, 2018. URL: https://doi.org/10.1007/s10817-017-9447-z.
  39. Natarajan Shankar. Towards mechanical metamathematics. Journal of Automated Reasoning, 1(4):407-434, 1985. Google Scholar
  40. Raymond M. Smullyan. First-Order Logic. Springer-Verlag, 1968. Google Scholar
  41. Alfred Tarski. Logic, Semantics, Metamathematics: Papers from 1923 to 1938. Hackett Publishing, 1983. Google Scholar
  42. Christian Urban. Nominal techniques in Isabelle/HOL. Journal of Automated Reasoning, 40(4):327-356, 2008. URL: https://doi.org/10.1007/s10817-008-9097-2.
  43. Wim Veldman. An intuitionistic completeness theorem for intuitionistic predicate logic. Journal of Symbolic Logic, 41(1):159-166, 1976. URL: https://doi.org/10.1017/S0022481200051859.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact