Completeness of First-Order Bi-Intuitionistic Logic

Authors Dominik Kirst , Ian Shillito



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.40.pdf
  • Filesize: 0.78 MB
  • 19 pages

Document Identifiers

Author Details

Dominik Kirst
  • Université Paris Cité, IRIF, Inria, Paris, France
  • Ben-Gurion University, Beer-Sheva, Israel
Ian Shillito
  • The Australian National University, Canberra, Ngunnawal & Ngambri Country, Australia

Cite As Get BibTex

Dominik Kirst and Ian Shillito. Completeness of First-Order Bi-Intuitionistic Logic. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.40

Abstract

We provide a succinct and verified completeness proof for first-order bi-intuitionistic logic, relative to constant domain Kripke semantics. By doing so, we make up for the almost-50-year-old substantial mistakes in Rauszer’s foundational work, detected but unresolved by Shillito two years ago. Moreover, an even earlier but historically neglected proof by Klemke has been found to contain at least local errors by Olkhovikov and Badia, that remained unfixed due to the technical complexity of Klemke’s argument. To resolve this unclear situation once and for all, we give a succinct completeness proof, based on and dualising a standard proof for constant domain intuitionistic logic, and verify our constructions using the Coq proof assistant to guarantee correctness.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
Keywords
  • bi-intuitionistic logic
  • first-order logic
  • completeness
  • Coq proof assistant

Metrics

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

References

  1. Sara Ayhan. Uniqueness of logical connectives in a bilateralist setting. In Martin Blicha and Igor Sedlár, editors, The Logica Yearbook 2020, pages 1-16. College Publications, 2021. URL: https://doi.org/10.48550/arXiv.2210.00989.
  2. Sara Ayhan. Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations. Journal of Logic and Computation, 2024. URL: https://doi.org/10.48550/arXiv.2307.01079.
  3. Sara Ayhan and Heinrich Wansing. On synonymy in proof-theoretic semantics. the case of 2int. Bulletin of the Section of Logic, 52(2), 2023. Google Scholar
  4. Thierry Coquand and Gérard Huet. The calculus of constructions. PhD thesis, INRIA, 1986. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  5. Tristan Crolard. Subtractive logic. TCS, 254:1-2:151-185, 2001. URL: https://doi.org/10.1016/S0304-3975(99)00124-3.
  6. Tristan Crolard. A formulae-as-types interpretation of subtractive logic. Journal of Logic and Computation, 14:4:529-570, 2004. URL: https://doi.org/10.1093/logcom/14.4.529.
  7. Nicolaas Govert De Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In Indagationes mathematicae (proceedings), volume 75(5), pages 381-392. Elsevier, 1972. Google Scholar
  8. Christian Doczkal and Joachim Bard. Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq. In Certified Programs and Proofs, Los Angeles, United States, January 2018. URL: https://doi.org/10.1145/3167088.
  9. Christian Doczkal and Gert Smolka. Completeness and decidability results for ctl in coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, pages 226-241, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-08970-6_15.
  10. Sergey Drobyshevich. A bilateral hilbert-style investigation of 2-intuitionistic logic. J. Log. Comput., 29(5):665-692, 2019. URL: https://doi.org/10.1093/logcom/exz010.
  11. Sergey Drobyshevich. Tarskian consequence relations bilaterally: some familiar notions. Synthese, 198(Suppl 22):5213-5240, 2021. URL: https://doi.org/10.1007/s11229-019-02267-w.
  12. Josep M. Font. Abstract Algebraic Logic: An Introductory Textbook. Studies in Logic and the Foundations of Mathematics. College Publications, 2016. Google Scholar
  13. 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. URL: https://doi.org/10.1145/3293880.3294091.
  14. 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. https://arxiv.org/abs/2006.04399, URL: https://doi.org/10.48550/arXiv.2006.04399.
  15. Dov M. Gabbay. Applications of trees to intermediate logics. Journal of Symbolic Logic, 37(1):135-138, 1972. URL: https://doi.org/10.2307/2272556.
  16. Dov M. Gabbay. Semantical investigations in Heyting’s intuitionistic logic, volume 148. D. Reidel Pub. Co, Dordrecht, Holland, 1981. Google Scholar
  17. Dov M. Gabbay, Valentin B. Shehtman, and Dmitrij P. Skvortsov. Quantification in Nonclassical Logic, volume 153. Elsevier, London, Amsterdam, 1st edition, 2009. Google Scholar
  18. Rajeev Goré and Ian Shillito. Bi-Intuitionistic Logics: A New Instance of an Old Problem. In Advances in Modal Logic 13, papers from the thirteenth conference on "Advances in Modal Logic," held online, 24-28 August 2020, pages 269-288, 2020. URL: http://www.aiml.net/volumes/volume13/Gore-Shillito.pdf.
  19. Andrzej Grzegorczyk. A philosophically plausible formal interpretation of intuitionistic logic. Indagationes Mathematicae, 26:596-601, 1964. Google Scholar
  20. Huayu Guo, Dongheng Chen, and Bruno Bentzen. Verified completeness in Henkin-style for intuitionistic propositional logic. In Bruno Bentzen, Beishui Liao, Davide Liga, Reka Markovich, Bin Wei, Minghui Xiong, and Tianwen Xu, editors, Joint Proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, September 8-9 and 11-12, 2023, Hangzhou, pages 36-48. College Publications, 2023. Google Scholar
  21. Christian Hagemeier and Dominik Kirst. Constructive and mechanised meta-theory of iel and similar modal logics. Journal of Logic and Computation, 32(8):1585-1610, 2022. URL: https://doi.org/10.1093/logcom/exac068.
  22. Hugo Herbelin and Dominik Kirst. New observations on the constructive content of first-order completeness theorems. In 29th International Conference on Types for Proofs and Programs, 2023. Google Scholar
  23. Marc Hermes and Dominik Kirst. An analysis of Tennenbaum’s theorem in constructive type theory. In International Conference on Formal Structures for Computation and Deduction. LIPIcs, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.9.
  24. Johannes Hostert, Andrej Dudenhefner, and Dominik Kirst. Undecidability of dyadic first-order logic in Coq. In International Conference on Interactive Theorem Proving. LIPIcs, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.19.
  25. Dominik Kirst. Mechanised Metamathematics: An Investigation of First-Order Logic and Set Theory in Constructive Type Theory. PhD thesis, Saarland University, 2022. Google Scholar
  26. Dominik Kirst and Marc Hermes. Synthetic undecidability and incompleteness of first-order axiom systems in Coq. In International Conference on Interactive Theorem Proving. LIPIcs, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.23.
  27. 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 Coq Workshop, 2022. Google Scholar
  28. Dominik Kirst and Dominique Larchey-Wendling. Trakhtenbrot’s theorem in Coq: Finite model theory through the constructive lens. Logical Methods in Computer Science, 18, 2022. URL: https://doi.org/10.46298/lmcs-18(2:17)2022.
  29. Dominik Kirst and Benjamin Peters. Gödel’s theorem without tears: Essential incompleteness in synthetic computability. In Annual conference of the European Association for Computer Science Logic. LIPIcs, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.30.
  30. Dieter Klemke. Ein Henkin-Beweis für die Vollständigkeit eines Kalküls relativ zur Grzegorczyk-Semantik. Archiv für mathematische Logik und Grundlagenforschung, 14:148-161, 1971. Google Scholar
  31. Marcus Kracht. Tools and Techniques in Modal Logic. Elsevier, 1999. Google Scholar
  32. E.G.K. López-Escobar. On intuitionistic sentential connectives I. Revista Colombiana de Matemáticas, 19(1-2):117-130, January 1985. Google Scholar
  33. Marco Maggesi and Cosimo Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.26.
  34. C. Moisil. Logique modale. Disquisitiones malhematicae et physicae, 2:3-98, 1942. Google Scholar
  35. Grigory K Olkhovikov and Guillermo Badia. Craig interpolation theorem fails in bi-intuitionistic predicate logic. The Review of Symbolic Logic, 17(2):611-633, 2024. URL: https://doi.org/10.1017/s1755020322000296.
  36. Hiroakira Ono. Craig’s Interpolation Theorem for the Intuitionistic Logic and Its Extensions: A Semantical Approach. Studia Logica: An International Journal for Symbolic Logic, 45(1):19-33, 1986. URL: https://doi.org/10.1007/BF01881546.
  37. 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. URL: https://doi.org/10.1007/BFb0037116.
  38. Luís Pinto and Tarmo Uustalu. Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents. In M. Giese and A. Waaler, editors, Proc. TABLEAUX, pages 295-309, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-02716-1_22.
  39. Arthur N. Prior. Time and Modality. Greenwood Press, Westport, Conn., 1955. Google Scholar
  40. Arthur N. Prior. Past, Present and Future. Clarendon P., Oxford,, 1967. Google Scholar
  41. Arthur N. Prior. Papers on Time and Tense. Oxford University Press UK, Oxford, England, 1968. Google Scholar
  42. Cecylia Rauszer. A Formalization of the Propositional Calculus of H-B Logic. Studia Logica: An International Journal for Symbolic Logic, 33(1):23-34, 1974. Google Scholar
  43. Cecylia Rauszer. Semi-Boolean algebras and their application to intuitionistic logic with dual operations. Fundamenta Mathematicae LXXXIII, pages 219-249, 1974. Google Scholar
  44. Cecylia Rauszer. On the Strong Semantical Completeness of Any Extension of the Intuitionistic Predicate Calculus. Bulletin de l'Académie Polonaise des Sciences, XXIV(2):81-87, 1976. Google Scholar
  45. Cecylia Rauszer. An algebraic approach to the Heyting-Brouwer predicate calculus. Fundamenta Mathematicae, 96(2):127-135, 1977. Google Scholar
  46. Cecylia Rauszer. Applications of Kripke Models to Heyting-Brouwer Logic. Studia Logica: An International Journal for Symbolic Logic, 36(1/2):61-71, 1977. Google Scholar
  47. Cecylia Rauszer. Model Theory for an Extension of Intuitionistic Logic. Studia Logica, 36(1-2):73-87, 1977. Google Scholar
  48. Cecylia Rauszer. An Algebraic and Kripke-Style Approach to a Certain Extension of Intuitionistic Logic. PhD thesis, Instytut Matematyczny Polskiej Akademi Nauk, 1980. Google Scholar
  49. Katsuhiko Sano and John G. Stell. Strong completeness and the finite model property for bi-intuitionistic stable tense logics. In Proc. Methods for Modalities 2017, volume 243 of Electronic Proceedings in Theoretical Computer Science, pages 105-121. Open Publishing Association, 2017. URL: https://doi.org/10.4204/EPTCS.243.8.
  50. Ian Shillito. New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq. PhD thesis, Australian National University, Canberra, 2023. Google Scholar
  51. Ian Shillito and Dominik Kirst. A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 218-229. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636957.
  52. Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 166-180, 2019. URL: https://doi.org/10.1145/3293880.3294101.
  53. The Coq Development Team. The coq proof assistant, June 2023. URL: https://doi.org/10.5281/zenodo.8161141.
  54. Heinrich Wansing. Falsification, natural deduction and bi-intuitionistic logic. J. Log. Comput., 26(1):425-450, 2016. URL: https://doi.org/10.1093/logcom/ext035.
  55. Heinrich Wansing. Connexive Logic. In Edward N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2023 edition, 2023. Google Scholar
  56. Benjamin Werner. Sets in types, types in sets. In International Symposium on Theoretical Aspects of Computer Software, pages 530-546. Springer, 1997. URL: https://doi.org/10.1007/BFb0014566.
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