Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents

Authors Tim S. Lyon , Ian Shillito , Alwen Tiu



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.41.pdf
  • Filesize: 0.89 MB
  • 23 pages

Document Identifiers

Author Details

Tim S. Lyon
  • Technische Universität Dresden, Germany
Ian Shillito
  • The Australian National University, Canberra, Ngunnawal & Ngambri Country, Australia
Alwen Tiu
  • The Australian National University, Canberra, Ngunnawal & Ngambri Country, Australia

Cite As Get BibTex

Tim S. Lyon, Ian Shillito, and Alwen Tiu. Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 41:1-41:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.41

Abstract

It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of models into a constant domain. This makes it an interesting problem to find a sound and complete proof system for first-order bi-intuitionistic logic with non-constant domains that is also conservative over first-order intuitionistic logic. We solve this problem by presenting the first sound and complete proof system for first-order bi-intuitionistic logic with increasing domains. We formalize our proof system as a polytree sequent calculus (a notational variant of nested sequents), and prove that it enjoys cut-elimination and is conservative over first-order intuitionistic logic. A key feature of our calculus is an explicit eigenvariable context, which allows us to control precisely the scope of free variables in a polytree structure. Semantically this context can be seen as encoding a notion of Scott’s existence predicate for intuitionistic logic. This turns out to be crucial to avoid the collapse of domains and to prove the completeness of our proof system. The explicit consideration of the variable context in a formula sheds light on a previously overlooked dependency between the residuation principle and the existence predicate in the first-order setting, which may help to explain the difficulty in designing a sound and complete proof system for first-order bi-intuitionistic logic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Constructive mathematics
  • Theory of computation → Automated reasoning
Keywords
  • Bi-intuitionistic
  • Cut-elimination
  • Conservativity
  • Domain
  • First-order
  • Polytree
  • Proof theory
  • Reachability
  • Sequent

Metrics

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

References

  1. Nuel D. Belnap. Display logic. Journal of philosophical logic, 11(4):375-417, 1982. URL: https://doi.org/10.1007/BF00284976.
  2. Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48(6):551-577, 2009. URL: https://doi.org/10.1007/s00153-009-0137-3.
  3. Robert A. Bull. Cut elimination for propositional dynamic logic without *. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 38(2):85-100, 1992. URL: https://doi.org/10.1002/MALQ.19920380107.
  4. Marcos A. Castilho, Luis Farinas del Cerro, Olivier Gasquet, and Andreas Herzig. Modal tableaux with propagation rules and structural rules. Fundamenta Informaticae, 32(3, 4):281-297, 1997. URL: https://doi.org/10.3233/FI-1997-323404.
  5. Agata Ciabattoni, Tim Lyon, Revantha Ramanayake, and Alwen Tiu. Display to labelled proofs and back again for tense logics. ACM Transactions on Computational Logic, 22(3):1-31, 2021. URL: https://doi.org/10.1145/3460492.
  6. Ranald Clouston, Jeremy E. Dawson, Rajeev Goré, and Alwen Tiu. Annotation-free sequent calculi for full intuitionistic linear logic - extended version. CoRR, abs/1307.0289, 2013. URL: https://arxiv.org/abs/1307.0289.
  7. 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.
  8. Melvin Fitting. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, 13(2):237-247, 1972. URL: https://doi.org/10.1305/NDJFL/1093894722.
  9. Melvin Fitting. Nested sequents for intuitionistic logics. Notre Dame Journal of Formal Logic, 55(1):41-61, 2014. URL: https://doi.org/10.1215/00294527-2377869.
  10. D. Gabbay, V. Shehtman, and D. Skvortsov. Quantification in Non-classical Logics. Studies in Logic and Foundations of Mathematics. Elsevier, Amsterdam, London, 2009. Google Scholar
  11. Gerhard Gentzen. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift, 39(1):176-210, 1935. Google Scholar
  12. Gerhard Gentzen. Untersuchungen über das logische Schließen. II. Mathematische Zeitschrift, 39(1):405-431, 1935. Google Scholar
  13. Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Carlos Areces and Robert Goldblatt, editors, Advances in Modal Logic 7, pages 43-66, Nancy, France, 2008. College Publications. URL: http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf.
  14. Rajeev Goré, Linda Postniece, and Alwen Tiu. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Logical Methods in Computer Science, 7(2):1-38, 2011. URL: https://doi.org/10.2168/LMCS-7(2:8)2011.
  15. Rajeev Goré and Ian Shillito. Bi-intuitionistic logics: A new instance of an old problem. In Advances in Modal Logic 13, pages 269-288, Helsinki, Finland, 2020. College Publications. URL: http://www.aiml.net/volumes/volume13/Gore-Shillito.pdf.
  16. Andrzej Grzegorczyk. A philosophically plausible formal interpretation of intuitionistic logic. Indagationes Mathematicae, 26(5):596-601, 1964. Google Scholar
  17. Ryo Ishigaki and Kentaro Kikuchi. Tree-sequent methods for subintuitionistic predicate logics. In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, volume 4548 of Lecture Notes in Computer Science, pages 149-164, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-73099-6_13.
  18. Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119-135, 1994. URL: https://doi.org/10.1007/BF01053026.
  19. Tim Lyon. On the correspondence between nested calculi and semantic systems for intuitionistic logics. Journal of Logic and Computation, 31(1):213-265, December 2020. URL: https://doi.org/10.1093/logcom/exaa078.
  20. Tim Lyon. Refining Labelled Systems for Modal and Constructive Logics with Applications. PhD thesis, Technische Universität Wien, 2021. Google Scholar
  21. Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston. Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, volume 152 of LIPIcs, pages 28:1-28:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.28.
  22. Tim S. Lyon. Nested sequents for intermediate logics: the case of Gödel-Dummett logics. Journal of Applied Non-Classical Logics, 33(2):121-164, 2023. URL: https://doi.org/10.1080/11663081.2023.2233346.
  23. Tim S. Lyon. Nested sequents for intermediate logics: The case of Gödel-Dummett logics, 2024. Updated version, on arXiv. URL: https://arxiv.org/abs/2306.07550, URL: https://doi.org/10.48550/arXiv.2306.07550.
  24. Tim S. Lyon and Lucía Gómez Álvarez. Automating reasoning with standpoint logic via nested sequents. In Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, pages 257-266, August 2022. URL: https://doi.org/10.24963/kr.2022/26.
  25. Tim S. Lyon and Jonas Karge. Constructive interpolation and concept-based beth definability for description logics via sequents. In Kate Larson, editor, Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24, pages 3484-3492. International Joint Conferences on Artificial Intelligence Organization, August 2024. Main Track. URL: https://www.ijcai.org/proceedings/2024/386, URL: https://doi.org/10.24963/ijcai.2024/386.
  26. Tim S. Lyon, Ian Shillito, and Alwen Tiu. Taking bi-intuitionistic logic first-order: A proof-theoretic investigation via polytree sequents, 2024. Appended version on arXiv. URL: https://arxiv.org/abs/2404.15855, URL: https://doi.org/10.48550/arXiv.2404.15855.
  27. E. G. K. López-Escobar. On the interpolation theorem for the logic of constant domains. Journal of Symbolic Logic, 46(1):87-88, 1981. URL: https://doi.org/10.2307/2273260.
  28. Sara Negri. Proof analysis in modal logic. Journal of Philosophical Logic, 34(5-6):507, 2005. Google Scholar
  29. Luís Pinto and Tarmo Uustalu. Relating sequent calculi for bi-intuitionistic propositional logic. In Steffen van Bakel, Stefano Berardi, and Ulrich Berger, editors, Proceedings Third International Workshop on Classical Logic and Computation, volume 47 of EPTCS, pages 57-72, 2010. URL: https://doi.org/10.4204/EPTCS.47.7.
  30. Luís Pinto and Tarmo Uustalu. A proof-theoretic study of bi-intuitionistic propositional sequent calculus. Journal of Logic and Computation, 28(1):165-202, 2018. URL: https://doi.org/10.1093/LOGCOM/EXX044.
  31. Linda Postniece. Deep inference in bi-intuitionistic logic. In Hiroakira Ono, Makoto Kanazawa, and Ruy de Queiroz, editors, Logic, Language, Information and Computation, pages 320-334, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-02261-6_26.
  32. Cecylia Rauszer. Applications of Kripke models to Heyting-Brouwer logic. Studia Logica, 36(1):61-71, 1977. URL: https://doi.org/10.1007/BF02121115.
  33. Cecylia Rauszer. An algebraic and Kripke-style approach to a certain extension of intuitionistic logic, dissertations mathematicae, 1980. Google Scholar
  34. Greg Restall. Constant domain quantified modal logics without boolean negation. Australasian Journal of Logic, 3:45-62, 2005. URL: https://doi.org/10.26686/ajl.v3i0.1772.
  35. Dana Scott. Identity and existence in intuitionistic logic. In Applications of Sheaves: Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra, and Analysis, Durham, July 9-21, 1977, pages 660-696. Springer, 2006. Google Scholar
  36. 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
  37. Alex K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh. College of Science and Engineering. School of Informatics, 1994. Google Scholar
  38. John G. Stell, Renate A. Schmidt, and David Rydeheard. A bi-intuitionistic modal logic: Foundations and automation. Journal of Logical and Algebraic Methods in Programming, 85(4):500-519, 2016. Relational and algebraic methods in computer science. URL: https://doi.org/10.1016/j.jlamp.2015.11.003.
  39. Gaisi Takeuti. Proof theory, volume 81. Courier Corporation, 2013. Google Scholar
  40. Alwen Tiu, Egor Ianovski, and Rajeev Goré. Grammar logics in nested sequent calculus: Proof theory and decision procedures. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence S. Moss, editors, Advances in Modal Logic 9, pages 516-537. College Publications, 2012. URL: http://www.aiml.net/volumes/volume9/Tiu-Ianovski-Gore.pdf.
  41. Luca Viganò. Labelled Non-Classical Logics. Springer Science & Business Media, 2000. 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