Document Open Access Logo

Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting

Authors Asta Halkjær From , Anders Schlichtkrull

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.8.pdf
  • Filesize: 0.77 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Higher order logic
Keywords
  • Logic
  • completeness
  • abstract consistency property
  • Isabelle/HOL
  • locales

Metrics

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

Abstract

Smullyan and Fitting have used abstract consistency properties to great effect in unifying meta-theoretical results in logic. In this paper, we generalize these developments with the help of Isabelle/HOL. We use locales to decompose abstract consistency into general parts, and provide the textbook variants as special cases. Users can assemble their own consistency property for a given logic. The compositionality alleviates the absence of dependent types in Isabelle/HOL. We use our development to mechanize completeness of calculi for three logics: (1) first-order logic where we only instantiate universal quantifiers with already occurring terms, (2) second-order logic over general models, and (3) a recently developed strong hybrid logic with propositional quantification.

Cite As Get BibTex

Asta Halkjær From and Anders Schlichtkrull. Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.8

Author Details

Asta Halkjær From
  • Department of Computer Science, University of Copenhagen, Denmark
Anders Schlichtkrull
  • Department of Computer Science, Aalborg University Copenhagen, Denmark

Funding

  • From, Asta Halkjær: This work is supported by a Novo Nordisk Fonden Start Package grant (NNF20OC0063462).

Acknowledgements

We thank the anonymous reviewers and Jørgen Villadsen for their comments.

Supplementary Materials

References

  1. Peter B. Andrews. An introduction to mathematical logic and type theory - to truth through proof. Computer science and applied mathematics. Academic Press, 1986. Google Scholar
  2. Clemens Ballarin. Locales: A module system for mathematical theories. Journal of Automated Reasoning, 52(2):123-153, 2014. URL: https://doi.org/10.1007/S10817-013-9284-7.
  3. Stefan Berghofer. First-order logic according to Fitting. Archive of Formal Proofs, 2007, August 2007. Formal proof development. URL: https://www.isa-afp.org/entries/FOL-Fitting.shtml.
  4. Patrick Blackburn, Torben Braüner, and Julie Lundbak Kofod. Prior’s ideal language. Mathematical Structures in Computer Science, 35, 2025. URL: https://doi.org/10.1017/S0960129525000076.
  5. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. Journal of Automated Reasoning, 51(1):109-128, 2013. URL: https://doi.org/10.1007/S10817-013-9278-5.
  6. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 93-110. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_7.
  7. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 111-127. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_8.
  8. 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.
  9. Anthony Bordg, Lawrence C. Paulson, and Wenda Li. Simple Type Theory is not too simple: Grothendieck’s schemes without dependent types. Exp. Math., 31(2):364-382, 2022. URL: https://doi.org/10.1080/10586458.2022.2062073.
  10. Torben Braüner. Hybrid Logic and its Proof-Theory. Springer, 1st edition, 2011. URL: https://doi.org/10.1007/978-94-007-0002-4.
  11. Joachim Breitner and Denis Lohner. The meta theory of the Incredible Proof Machine. Archive of Formal Proofs, 2016, May 2016. Formal proof development. URL: https://www.isa-afp.org/entries/Incredible_Proof_Machine.shtml.
  12. Javier Díaz. Metatheory of Q0. Archive of Formal Proofs, 2023, November 2023. Formal proof development. URL: https://www.isa-afp.org/entries/Q0_Metatheory.html.
  13. Matthew Doty. Class-based classical propositional logic. Archive of Formal Proofs, 2022, December 2022. Formal proof development. URL: https://www.isa-afp.org/entries/Propositional_Logic_Class.html.
  14. Melvin Fitting. Model existence theorems for modal and intuitionistic logics. Journal of Symbolic Logic, 38(4):613-627, 1973. URL: https://doi.org/10.2307/2271986.
  15. Melvin Fitting. First-Order Logic and Automated Theorem Proving, Second Edition. Graduate Texts in Computer Science. Springer, 1996. URL: https://doi.org/10.1007/978-1-4612-2360-3.
  16. Melvin Fitting, Lars Thalmann, and Andrei Voronkov. Term-modal logics. Studia Logica, 69(1):133-169, 2001. URL: https://doi.org/10.1023/A:1013842612702.
  17. 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.
  18. Asta Halkjær From. Soundness and completeness of an axiomatic system for first-order logic. Archive of Formal Proofs, 2021, September 2021. Formal proof development. URL: https://www.isa-afp.org/entries/FOL_Axiomatic.html.
  19. Asta Halkjær From. A naive prover for first-order logic. Archive of Formal Proofs, 2022, March 2022. Formal proof development. URL: https://www.isa-afp.org/entries/FOL_Seq_Calc3.html.
  20. Asta Halkjær From. An Isabelle/HOL framework for synthetic completeness proofs. In Kathrin Stark, Amin Timany, Sandrine Blazy, and Nicolas Tabareau, editors, Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2025, Denver, CO, USA, January 20-21, 2025, CPP '25, pages 171-186, New York, NY, USA, 2025. ACM. URL: https://doi.org/10.1145/3703595.3705882.
  21. Asta Halkjær From and Frederik Krogsdal Jacobsen. A sequent calculus prover for first-order logic with functions. Archive of Formal Proofs, 2022, January 2022. Formal proof development. URL: https://www.isa-afp.org/entries/FOL_Seq_Calc2.html.
  22. Asta Halkjær From and Frederik Krogsdal Jacobsen. Verifying a sequent calculus prover for first-order logic with functions in Isabelle/HOL. Journal of Automated Reasoning, 68(3):15, 2024. URL: https://doi.org/10.1007/S10817-024-09697-3.
  23. Asta Halkjær From and Anders Schlichtkrull. Analytic Completeness. Software, version 1.0., (visited on 2025-09-03). URL: https://github.com/astahfrom/Analytic_Completeness
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23798
  24. Asta Halkjær From. A succinct formalization of the completeness of first-order logic. In Henning Basold, Jesper Cockx, and Silvia Ghilezan, editors, 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference), volume 239 of LIPIcs, pages 8:1-8:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.TYPES.2021.8.
  25. 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.
  26. Leon Henkin. The discovery of my completeness proofs. Bulletin of Symbolic Logic, 2(2):127-158, 1996. URL: https://doi.org/10.2307/421107.
  27. Dominik Kirst and Marc Hermes. Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Journal of Automated Reasoning, 67(1):13, 2023. URL: https://doi.org/10.1007/S10817-022-09647-X.
  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. Mark Koch. Mechanizing second-order logic in Coq. Bachelor’s thesis, Saarland University, 2021. Google Scholar
  30. Mark Koch and Dominik Kirst. Undecidability, incompleteness, and completeness of second-order logic in Coq. In Andrei Popescu and Steve Zdancewic, editors, CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pages 274-290. ACM, 2022. URL: https://doi.org/10.1145/3497775.3503684.
  31. Julius Michaelis and Tobias Nipkow. Propositional proof systems. Archive of Formal Proofs, 2017, June 2017. Formal proof development. URL: https://www.isa-afp.org/entries/Propositional_Proof_Systems.shtml.
  32. 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 1-16, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Paper 5. URL: https://doi.org/10.4230/LIPIcs.TYPES.2017.5.
  33. Richard Montague. Reductions of higher-order logic. In J.W. Addison, Leon Henkin, and Alfred Tarski, editors, The Theory of Models: Proceedings of the 1963 International Symposium at Berkeley, Studies in Logic and the Foundations of Mathematics, pages 251-264. North-Holland, 1963. URL: https://doi.org/10.1016/B978-0-7204-2233-7.50030-7.
  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. Marius Petria. An institutional version of Gödel’s completeness theorem. In Till Mossakowski, Ugo Montanari, and Magne Haveraaen, editors, Algebra and Coalgebra in Computer Science, Second International Conference, CALCO 2007, Bergen, Norway, August 20-24, 2007, Proceedings, volume 4624 of Lecture Notes in Computer Science, pages 409-424. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73859-6_28.
  36. Anders Schlichtkrull. Soundness of the Q0 proof system for higher-order logic. Archive of Formal Proofs, 2023, November 2023. Formal proof development. URL: https://www.isa-afp.org/entries/Q0_Soundness.html.
  37. Julian J. Schlöder and Peter Koepke. The Gödel completeness theorem for uncountable languages. Formalized Mathematics, 20(3):199-203, 2012. URL: https://doi.org/10.2478/v10037-012-0023-z.
  38. Fabián Fernando Serrano Suárez, Mauricio Ayala-Rincón, and Thaynara Arielly de Lima. Hall’s theorem for enumerable families of finite sets. In Kevin Buzzard and Temur Kutsia, editors, Intelligent Computer Mathematics, pages 107-121, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-031-16681-5_7.
  39. Raymond M. Smullyan. A unifying principal in quantification theory. Proceedings of the National Academy of Sciences, 49(6):828-832, 1963. URL: https://doi.org/10.1073/pnas.49.6.828.
  40. Raymond M. Smullyan. First-Order Logic. Springer, Berlin, 1968. URL: https://doi.org/10.1007/978-3-642-86718-7.
  41. Fabián Fernando Serrano Suárez, Thaynara Arielly de Lima, and Mauricio Ayala-Rincón. Compactness theorem for propositional logic and combinatorial applications. Archive of Formal Proofs, 2024, August 2024. Formal proof development. URL: https://www.isa-afp.org/entries/Prop_Compactness.html.
  42. Sophie Tourret and Lawrence C. Paulson. Compactness theorem for first-order logic. Archive of Formal Proofs, 2025, February 2025. Formal proof development. URL: https://www.isa-afp.org/entries/FOL_Compactness.html.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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