Document Open Access Logo

The Flower Calculus

Author Pablo Donato

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.5.pdf
  • Filesize: 1.19 MB
  • 24 pages

Document Identifiers

Author Details

Pablo Donato
  • LIX, École Polytechnique, Palaiseau, France

Acknowledgements

I want to thank Luc Chabassier for writing the Lua script that was used to generate all the flower drawings in this document, and Benjamin Werner for useful feedback on a first draft of this paper. Lastly, I thank Tito for teaching me some invaluable formatting tricks.

Cite AsGet BibTex

Pablo Donato. The Flower Calculus. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 5:1-5:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.5

Abstract

We introduce the flower calculus, a deep inference proof system for intuitionistic first-order logic inspired by Peirce’s existential graphs. It works as a rewriting system over inductive objects called "flowers", that enjoy both a graphical interpretation as topological diagrams, and a textual presentation as nested sequents akin to coherent formulas. Importantly, the calculus dispenses completely with the traditional notion of symbolic connective, operating solely on nested flowers containing atomic predicates. We prove both the soundness of the full calculus and the completeness of an analytic fragment with respect to Kripke semantics. This provides to our knowledge the first analyticity result for a proof system based on existential graphs, adapting semantic cut-elimination techniques to a deep inference setting. Furthermore, the kernel of rules targetted by completeness is fully invertible, a desirable property for both automated and interactive proof search.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Constructive mathematics
Keywords
  • deep inference
  • graphical calculi
  • existential graphs
  • intuitionistic logic
  • Kripke semantics
  • cut-elimination

Metrics

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

Related Versions

Supplementary Materials

References

  1. Samson Abramsky and Achim Jung. Domain Theory. Oxford University Press, Inc., USA, 1995. Google Scholar
  2. Edward W. Ayers. A Tool for Producing Verified, Explainable Proofs. PhD thesis, University of Cambridge, 2021. Google Scholar
  3. Edward W. Ayers, Mateja Jamnik, and W. T. Gowers. A Graphical User Interface Framework for Formal Verification. 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 4:1-4:16, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.4.
  4. Yves Bertot, Gilles Kahn, and Laurent Théry. Proof by pointing. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, volume 789, pages 141-160. Springer Berlin Heidelberg, 1994. Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/3-540-57887-0_94.
  5. Marc Bezem and Thierry Coquand. Automating Coherent Logic. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, pages 246-260, Berlin, Heidelberg, 2005. Springer. URL: https://doi.org/10.1007/11591191_18.
  6. Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, and Pawel Sobocinski. Diagrammatic Algebra of First Order Logic, January 2024. arXiv:2401.07055 [cs, math]. URL: https://doi.org/10.48550/arXiv.2401.07055.
  7. Geraldine Brady and Todd H. Trimble. A categorical interpretation of C.S. Peirce’s propositional logic Alpha. Journal of Pure and Applied Algebra, 149(3):213-239, June 2000. URL: https://doi.org/10.1016/S0022-4049(98)00179-0.
  8. Geraldine Brady and Todd H. Trimble. A String Diagram Calculus for Predicate Logic and C. S. Peirce’s System Beta, June 2000. URL: https://ncatlab.org/nlab/files/BradyTrimbleString.pdf.
  9. Taus Brock-Nannestad and Danko Ilik. An Intuitionistic Formula Hierarchy Based on High-School Identities. Mathematical Logic Quarterly, 65(1):57-79, May 2019. arXiv: 1601.04876. URL: https://doi.org/10.1002/malq.201700047.
  10. Paola Bruscoli and Alessio Guglielmi. On Analyticity in Deep Inference. Mathematical Structures in Computer Science, 29(Special Issue 8: A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller’s 60th birthday), 2019. URL: https://doi.org/10.1017/S0960129519000136.
  11. Gianluca Caterina and Rocco Gangle. A New Syntax for Diagrammatic Logic: A Generic Figures Approach. In Yaroslav D. Sergeyev and Dmitri E. Kvasov, editors, Numerical Computations: Theory and Algorithms, Lecture Notes in Computer Science, pages 43-58, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-40616-5_4.
  12. Kaustuv Chaudhuri. Subformula linking as an interaction method. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, volume 7998, pages 386-401. Springer Berlin Heidelberg, 2013. Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/978-3-642-39634-2_28.
  13. Kaustuv Chaudhuri. Subformula linking for intuitionistic logic with application to type theory. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 200-216. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_12.
  14. Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Modular focused proof systems for intuitionistic modal logics. In International Conference on Formal Structures for Computation and Deduction, 2016. Google Scholar
  15. Ranald Clouston, Jeremy Dawson, Rajeev Goré, and Alwen Tiu. Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), volume 23 of Leibniz International Proceedings in Informatics (LIPIcs), pages 197-214, Dagstuhl, Germany, 2013. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.197.
  16. Sharon Curtis and Gavin Lowe. Proofs with graphs. Science of Computer Programming, 26(1):197-216, May 1996. URL: https://doi.org/10.1016/0167-6423(95)00025-9.
  17. Renata De Freitas, Paulo A. S. Veloso, Sheila R. M. Veloso, and Petrucio Viana. On graph reasoning. Information and Computation, 207(10):1000-1014, October 2009. URL: https://doi.org/10.1016/j.ic.2008.11.004.
  18. Renata De Freitas, Paulo A. S. Veloso, Sheila R. M. Veloso, and Petrucio Viana. A Calculus for Graphs with Complement. In Ashok K. Goel, Mateja Jamnik, and N. Hari Narayanan, editors, Diagrammatic Representation and Inference, volume 6170, pages 84-98. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010. Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/978-3-642-14600-8_11.
  19. Pablo Donato. flowers-metatheory, November 2022. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:290076a847ca95e93c17fb66659086d7f68be014;origin=https://github.com/Champitoad/flowers-metatheory;visit=swh:1:snp:4e8e9db020ad62996ea53e2f7aa11a1293700d6c;anchor=swh:1:rev:9fad86b89037ce4aca7ffefc9a964a39ee3e473d (visited on 2024-06-20). URL: https://github.com/Champitoad/flowers-metatheory.
  20. Pablo Donato. flower-prover, October 2023. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:fcc934cae3a75692c031dc82ffdab138084a472d;origin=https://github.com/Champitoad/flower-prover;visit=swh:1:snp:25cb9a170bf72700948f6d30840e8593c52316a5;anchor=swh:1:rev:a14d2f0c6b4ff596eb5169115ef454b86080361b (visited on 2024-06-20). URL: https://github.com/Champitoad/flower-prover.
  21. Pablo Donato. The Flower Calculus. Preprint, April 2024. URL: https://arxiv.org/abs/2402.15174.
  22. Pablo Donato, Pierre-Yves Strub, and Benjamin Werner. A drag-and-drop proof tactic. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022, pages 197-209, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3497775.3503692.
  23. 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.
  24. M. Ganesalingam and W. T. Gowers. A Fully Automatic Theorem Prover with Human-Style Output. Journal of Automated Reasoning, 58(2):253-291, February 2017. URL: https://doi.org/10.1007/s10817-016-9377-1.
  25. Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales, and Lutz Straßburger. Intuitionistic S4 is decidable. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, June 2023. arXiv:2304.12094 [cs]. URL: https://doi.org/10.1109/LICS56636.2023.10175684.
  26. Nicolas Guenot. Nested Deduction in Logical Foundations for Computation. PhD thesis, Ecole Polytechnique X, April 2013. URL: https://pastel.archives-ouvertes.fr/pastel-00929908.
  27. Nathan Haydon and Paweł Sobociński. Compositional Diagrammatic First-Order Logic. In Ahti-Veikko Pietarinen, Peter Chapman, Leonie Bosveld-de Smet, Valeria Giardino, James Corter, and Sven Linker, editors, Diagrammatic Representation and Inference, volume 12169, pages 402-418. Springer International Publishing, Cham, 2020. Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/978-3-030-54249-8_32.
  28. Olivier Hermant. Semantic Cut Elimination in the Intuitionistic Sequent Calculus. In David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Dough Tygar, Moshe Y. Vardi, Gerhard Weikum, and Paweł Urzyczyn, editors, Typed Lambda Calculi and Applications, volume 3461, pages 221-233. Springer Berlin Heidelberg, Berlin, Heidelberg, 2005. Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/11417170_17.
  29. John Howse, Gem Stapleton, and John Taylor. Spider Diagrams. LMS Journal of Computation and Mathematics, 8:145-194, January 2005. Publisher: Cambridge University Press. URL: https://doi.org/10.1112/S1461157000000942.
  30. Predrag Janičić and Julien Narboux. Automated generation of illustrated proofs in geometry and beyond. Annals of Mathematics and Artificial Intelligence, July 2023. URL: https://doi.org/10.1007/s10472-023-09857-y.
  31. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium, volume 2 of Oxford Logic Guides. Clarendon Press, Oxford, England, September 2002. Google Scholar
  32. Roman Kuznets and Lutz Straßburger. Maehara-style modal nested calculi. Archive for Mathematical Logic, 58(3-4):359-385, May 2019. URL: https://doi.org/10.1007/s00153-018-0636-1.
  33. Marie La Palme Reyes, Gonzalo E. Reyes, and Houman Zolfaghari. Generic figures and their glueings. Polimetrica, International Scientific Publisher, 2008. Google Scholar
  34. C. I. Lewis. A survey of symbolic logic. Journal of Philosophy, Psychology and Scientific Methods, 17(3):78-79, 1920. URL: https://doi.org/10.2307/2940631.
  35. Sven Linker, Jim Burton, and Mateja Jamnik. Tactical Diagrammatic Reasoning. Electronic Proceedings in Theoretical Computer Science, 239:29-42, January 2017. URL: https://doi.org/10.4204/EPTCS.239.3.
  36. Tim Lyon. Refining Labelled Systems for Modal and Constructive Logics with Applications. PhD thesis, Vienna University of Technology, July 2021. URL: https://doi.org/10.48550/arXiv.2107.14487.
  37. Tim S. Lyon. Nested Sequents for Intuitionistic Modal Logics via Structural Refinement. In Anupam Das and Sara Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Computer Science, pages 409-427, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-86059-2_24.
  38. Thomas Långbacka, Rimvydas Rukšėnas, and Joakim von Wright. TkWinHOL: A tool for Window Inference in HOL. In E. Thomas Schubert, Philip J. Windley, and James Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science, pages 245-260, Berlin, Heidelberg, 1995. Springer. URL: https://doi.org/10.1007/3-540-60275-5_69.
  39. Minghui Ma and Ahti-Veikko Pietarinen. Proof Analysis of Peirce’s Alpha System of Graphs. Studia Logica, 105(3):625-647, June 2017. URL: https://doi.org/10.1007/s11225-016-9703-y.
  40. Minghui Ma and Ahti-Veikko Pietarinen. A graphical deep inference system for intuitionistic logic. Logique et Analyse, 245:73-114, January 2019. URL: https://doi.org/10.2143/LEA.245.0.3285706.
  41. Sonia Marin, Dale Miller, Elaine Pimentel, and Marco Volpe. From axioms to synthetic inference rules via focusing. Annals of Pure and Applied Logic, 173(5):103091, May 2022. URL: https://doi.org/10.1016/j.apal.2022.103091.
  42. Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, July 2000. URL: https://era.ed.ac.uk/handle/1842/374.
  43. Paul-André Melliès and Noam Zeilberger. A bifibrational reconstruction of Lawvere’s presheaf hyperdoctrine. arXiv:1601.06098 [cs, math], August 2016. URL: https://arxiv.org/abs/1601.06098.
  44. Robin Milner. The use of machines to assist in rigorous proof. Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences, 312(1522):411-422, 1984. URL: https://doi.org/10.1098/rsta.1984.0067.
  45. Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28, pages 625-635, Cham, 2021. Springer International Publishing. Google Scholar
  46. Arnold Oostra. Los gráficos Alfa de Peirce aplicados a la lógica intuicionista. Number 2 in Cuadernos de Sistemática Peirceana. Centro de Sistemática Peirceana, 2010. Google Scholar
  47. Arnold Oostra. Gráficos existenciales Beta intuicionistas. Number 3 in Cuadernos de Sistemática Peirceana. Centro de Sistemática Peirceana, 2011. Google Scholar
  48. Arnold Oostra. Equivalence proof for intuitionistic existential alpha graphs. In Diagrammatic Representation and Inference: 12th International Conference, Diagrams 2021, Virtual, September 28–30, 2021, Proceedings, pages 188-195, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-86062-2_16.
  49. Arnold Oostra. Advances in Peircean Mathematics: The Colombian School, chapter Intuitionistic and Geometrical Extensions of Peirce’s Existential Graphs, pages 105-180. De Gruyter, 2022. Google Scholar
  50. Charles Sanders Peirce. Prolegomena to an Apology for Pragmaticism. The Monist, 16(4):492-546, 1906. Publisher: Oxford University Press. URL: https://www.jstor.org/stable/27899680.
  51. Brian Ritchie. The Design and Implementation of an Interactive Proof Editor. PhD thesis, The University of Edinburgh, 1988. Accepted: 2013-04-02T15:18:04Z Publisher: The University of Edinburgh. URL: https://era.ed.ac.uk/handle/1842/6607.
  52. Don D. Roberts. The Existential Graphs of Charles S. Peirce. De Gruyter Mouton, Berlin, Boston, 1973. URL: https://doi.org/doi:10.1515/9783110226225.
  53. Benoit Rognier and Guillaume Duhamel. Présentation de la plateforme edukera. In Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), 2016. Google Scholar
  54. Sun-Joo Shin. The Iconic Logic of Peirce’s Graphs. The MIT Press, May 2002. URL: https://doi.org/10.7551/mitpress/3633.001.0001.
  55. Thoralf Skolem. Logisch-kombinatorische untersuchungen Über die erfüllbarkeit oder bewiesbarkeit mathematischer sätze nebst einem theorem Über dichte mengen. In Thoralf Skolem, editor, Selected Works in Logic. Universitetsforlaget, 1920. Google Scholar
  56. John Sowa. Peirce’s Tutorial on Existential Graphs. Semiotica, 186:345-394, 2011. URL: https://doi.org/10.1515/semi.2011.060.
  57. M. H. Stone. Topological representations of distributive lattices and Brouwerian logics. In Časopis pro pěstování matematiky a fysiky, volume 067, pages 1-25, 1938. ISSN: 1802-114X Issue: 1 Journal Abbreviation: Časopis Pěst. Mat. Fys. URL: https://doi.org/10.21136/CPMF.1938.124080.
  58. The Coq Development Team. The Coq Proof Assistant, 2022. URL: https://doi.org/10.5281/zenodo.7313584.
  59. Alwen Tiu. A Local System for Intuitionistic Logic. In Miki Hermann and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, pages 242-256, Berlin, Heidelberg, 2006. Springer. URL: https://doi.org/10.1007/11916277_17.
  60. Paulo Veloso, Sheila Veloso, and Mario Benevides. On Graph Calculi for Multi-modal Logics. Electronic Notes in Theoretical Computer Science, 312, April 2015. URL: https://doi.org/10.1016/j.entcs.2015.04.014.
  61. Paulo A. S. Veloso, Sheila R. M. Veloso, and Mario R. F. Benevides. PDL for structured data: a graph-calculus approach. Logic Journal of the IGPL, 22(5):737-757, October 2014. URL: https://doi.org/10.1093/jigpal/jzu011.
  62. Paulo A. S. Veloso, Sheila R. M. Veloso, and Mario R. F. Benevides. On a graph calculus for modalities. Theoretical Computer Science, 685:83-103, July 2017. URL: https://doi.org/10.1016/j.tcs.2016.11.037.
  63. Burghard Von Karger and C. A. R. Hoare. Sequential calculus. Information Processing Letters, 53(3):123-130, February 1995. URL: https://doi.org/10.1016/0020-0190(94)00205-D.
  64. Fernando Zalamea. Lógica topológica. una introducción a los gráficos existenciales de peirce. Memorias del XIV Coloquio Distrital de Matemáticas y Estadística, 1997. Google Scholar
  65. Fernando Zalamea. Pragmaticismo, gráficos y continuidad. hacia el lugar de c. s. peirce en la historia de la lógica. Mathesis 13, pp. 147–156, 1997. Google Scholar
  66. Fernando Zalamea. Peirce’s logic of continuity: Existential graphs and non-Cantorian continuum. Review of Modern Logic, 9(1-2):115-162, January 2003. Publisher: The Review of Modern Logic. URL: https://projecteuclid.org/journals/review-of-modern-logic/volume-9/issue-1-2/Peirces-logic-of-continuity--Existential-graphs-and-non-Cantorian/rml/1081173838.full.
  67. J.J. Zeman. The Graphical Logic of C. S. Peirce. PhD thesis, University of Chicago, 1964. URL: https://books.google.fr/books?id=E0AqAQAAMAAJ.
  68. Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou, and Wenhui Sun. Design of point-and-click user interfaces for proof assistants. In Formal Methods and Software Engineering: 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5–9, 2019, Proceedings, pages 86-103, Berlin, Heidelberg, 2019. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-32409-4_6.
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