Document Open Access Logo

When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines

Authors Filippo Bonchi, Alessandro Di Giorgio , Davide Trotta

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2024.30.pdf
  • Filesize: 0.9 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Categorical semantics
Keywords
  • relational algebra
  • hyperdoctrines
  • cartesian bicategories
  • string diagrams

Metrics

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

Abstract

Fo-bicategories are a categorification of Peirce’s calculus of relations. Notably, their laws provide a proof system for first-order logic that is both purely equational and complete. This paper illustrates a correspondence between fo-bicategories and Lawvere’s hyperdoctrines. To streamline our proof, we introduce peircean bicategories, which offer a more succinct characterization of fo-bicategories.

Cite As Get BibTex

Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta. When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.MFCS.2024.30

Author Details

Filippo Bonchi
  • University of Pisa, Italy
Alessandro Di Giorgio
  • University College London, UK
Davide Trotta
  • University of Padova, Italy

Funding

  • Bonchi, Filippo: Supported by MUR project PRIN 2022 PNRR No. P2022HXNSC - RAP (Resource Awareness in Programming) and University of Pisa project PRA_2022_99 - FM4HD.
  • Di Giorgio, Alessandro: Supported by EPSRC project EP/V002376/1 - Nominal String Diagrams.

References

  1. Richard Bird and Oege De Moor. The algebra of programming. NATO ASI DPD, 152:167-203, 1996. Google Scholar
  2. Benedikt Bollig, Alain Finkel, and Amrita Suresh. Bounded Reachability Problems Are Decidable in FIFO Machines. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of Leibniz International Proceedings in Informatics (LIPIcs), pages 49:1-49:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.49.
  3. Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, and Pawel Sobocinski. Diagrammatic algebra of first order logic. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '24, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3661814.3662078.
  4. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory I: rewriting with frobenius structure. J. ACM, 69(2):14:1-14:58, 2022. URL: https://doi.org/10.1145/3502719.
  5. Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta. When lawvere meets peirce: an equational presentation of boolean hyperdoctrines, 2024. URL: https://arxiv.org/abs/2404.18795.
  6. Filippo Bonchi, Joshua Holland, Robin Piedeleu, Paweł Sobociński, and Fabio Zanasi. Diagrammatic algebra: From linear to concurrent systems. Proceedings of the ACM on Programming Languages, 3(POPL):25:1-25:28, January 2019. URL: https://doi.org/10.1145/3290338.
  7. Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński. On doctrines and cartesian bicategories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  8. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full Abstraction for Signal Flow Graphs. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 515-526, New York, NY, USA, January 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2676726.2676993.
  9. George Boole. The mathematical analysis of logic. Philosophical Library, 1847. Google Scholar
  10. Geraldine Brady and Todd Trimble. A categorical interpretation of c.s. peirce’s propositional logic alpha. Journal of Pure and Applied Algebra - J PURE APPL ALG, 149:213-239, June 2000. URL: https://doi.org/10.1016/S0022-4049(98)00179-0.
  11. A. Carboni and R. F. C. Walters. Cartesian bicategories I. Journal of Pure and Applied Algebra, 49(1):11-32, November 1987. URL: https://doi.org/10.1016/0022-4049(87)90121-6.
  12. J. Robin B. Cockett, Jürgen Koslowski, and Robert AG Seely. Introduction to linear bicategories. Mathematical Structures in Computer Science, 10(2):165-203, 2000. Google Scholar
  13. Edgar Frank Codd. A relational model of data for large shared data banks. Communications of the ACM, 26(1):64-69, 1983. Google Scholar
  14. Bob Coecke and Ross Duncan. Interacting quantum observables: Categorical algebra and diagrammatics. New Journal of Physics, 13(4):043016, April 2011. URL: https://doi.org/10.1088/1367-2630/13/4/043016.
  15. Francesco Dagnino and Fabio Pasquali. Quotients and Extensionality in Relational Doctrines. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), volume 260 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:23, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2023.25.
  16. Augustus De Morgan. On the syllogism, no. iv. and on the logic of relations. Printed by C.J. Clay at the University Press, 1860. Google Scholar
  17. Charles J Everett and Stanislaw Ulam. Projective algebra i. American Journal of Mathematics, 68(1):77-88, 1946. Google Scholar
  18. William Ewald. The emergence of first-order logic. Stanford Encyclopedia of Philosophy, 2018. Google Scholar
  19. Brendan Fong, Paweł Sobociński, and Paolo Rapisarda. A categorical approach to open and interconnected dynamical systems. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 495-504, New York, NY, USA, July 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2933575.2934556.
  20. Brendan Fong and David Spivak. String diagrams for regular logic (extended abstract). In John Baez and Bob Coecke, editors, Applied Category Theory 2019, volume 323 of Electronic Proceedings in Theoretical Computer Science, pages 196-229. Open Publishing Association, September 2020. URL: https://doi.org/10.4204/eptcs.323.14.
  21. GOTTLOB FREGE. Begriffsschrift und andere Aufsätze. Georg Olms Verlag, 1977. Google Scholar
  22. Peter Freyd and Andre Scedrov. Categories, Allegories, volume 39 of North-Holland Mathematical Library. Elsevier B.V, 1990. Google Scholar
  23. CARSTEN FÜHRMANN and DAVID PYM. On categorical models of classical logic and the geometry of interaction. Mathematical Structures in Computer Science, 17(5):957-1027, 2007. URL: https://doi.org/10.1017/S0960129507006287.
  24. Dan R. Ghica and Achim Jung. Categorical semantics of digital circuits. In 2016 Formal Methods in Computer-Aided Design (FMCAD), pages 41-48, 2016. URL: https://doi.org/10.1109/FMCAD.2016.7886659.
  25. Nathan Haydon and Paweł Sobociński. Compositional diagrammatic first-order logic. In 11th International Conference on the Theory and Application of Diagrams (DIAGRAMS 2020), 2020. Google Scholar
  26. Leon Henkin. Cylindric algebras, 1971. Google Scholar
  27. CAR Hoare and He Jifeng. The weakest prespecification, part i. Fundamenta Informaticae, 9(1):51-84, 1986. Google Scholar
  28. Ian Hodkinson and Szabolcs Mikulás. Axiomatizability of reducts of algebras of relations. Algebra Universalis, 43(2):127-156, August 2000. URL: https://doi.org/10.1007/s000120050150.
  29. J.M.E. Hyland, P.T. Johnstone, and A.M. Pitts. Tripos theory. Math. Proc. Camb. Phil. Soc., 88:205-232, 1980. Google Scholar
  30. Martin Hyland. Abstract interpretation of proofs: Classical propositional calculus. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, pages 6-21, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  31. B. Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the foundations of mathematics. North Holland Publishing Company, 1999. Google Scholar
  32. P.T. Johnstone. Topos Theory. cademic Press, 1977. Google Scholar
  33. P.T. Johnstone. Sketches of an elephant: a topos theory compendium, volume 2 of Studies in Logic and the foundations of mathematics. Oxford Univ. Press, 2002. Google Scholar
  34. André Joyal and Ross Street. The geometry of tensor calculus, I. Advances in Mathematics, 88(1):55-112, July 1991. URL: https://doi.org/10.1016/0001-8708(91)90003-P.
  35. Petrus Marinus Waltherus Knijnenburg and Frank Nordemann. Two Categories of Relations. Citeseer, 1994. Google Scholar
  36. Alexander Krauss and Tobias Nipkow. Proof pearl: Regular expression equivalence and relation algebra. Journal of Automated Reasoning, 49(1):95-106, 2012. URL: https://doi.org/10.1007/s10817-011-9223-4.
  37. Ugo Dal Lago and Francesco Gavazzo. A relational theory of effects and coeffects. Proc. ACM Program. Lang., 6(POPL):1-28, 2022. URL: https://doi.org/10.1145/3498692.
  38. Søren B Lassen. Relational reasoning about contexts. Higher order operational techniques in semantics, 91, 1998. Google Scholar
  39. F. W. Lawvere. Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, New York, NY, USA, 1963. Google Scholar
  40. F.W. Lawvere. Adjointness in foundations. Dialectica, 23:281-296, 1969. Google Scholar
  41. F.W. Lawvere. Diagonal arguments and cartesian closed categories. In Category Theory, Homology Theory and their Applications, volume 2, pages 134-145. Springer, 1969. Google Scholar
  42. F.W. Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In A. Heller, editor, New York Symposium on Application of Categorical Algebra, volume 2, pages 1-14. American Mathematical Society, 1970. Google Scholar
  43. Leopold Löwenheim. Über Möglichkeiten im Relativkalkül. Mathematische Annalen, 76(4):447-470, 1915. Google Scholar
  44. M.E. Maietti, F. Pasquali, and G. Rosolini. Triposes, exact completions, and hilbert’s ε-operator. Tbilisi Mathematica journal, 10(3):141-166, 2017. Google Scholar
  45. M.E. Maietti and G. Rosolini. Elementary quotient completion. Theory App. Categ., 27(17):445-463, 2013. Google Scholar
  46. M.E. Maietti and G. Rosolini. Quotient completion for the foundation of constructive mathematics. Log. Univers., 7(3):371-402, 2013. Google Scholar
  47. M.E. Maietti and G. Rosolini. Unifying exact completions. Appl. Categ. Structures, 23:43-52, 2013. Google Scholar
  48. M.E. Maietti and D. Trotta. A characterization of generalized existential completions. Annals of Pure and Applied Logic, 174(4):103234, 2023. Google Scholar
  49. Paul-André Melliès. Dialogue categories and chiralities. Publications of the Research Institute for Mathematical Sciences, 52(4):359-412, 2016. Google Scholar
  50. Paul-André Melliès and Noam Zeilberger. A bifibrational reconstruction of lawvere’s presheaf hyperdoctrine. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 555-564, 2016. Google Scholar
  51. Donald Monk. On representable relation algebras. Michigan Mathematical Journal, 11(3):207-210, 1964. URL: https://doi.org/10.1307/mmj/1028999131.
  52. Koko Muroya, Steven W. T. Cheung, and Dan R. Ghica. The geometry of computation-graph abstraction. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 749-758. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209127.
  53. Jean-Pierre Olivier and Dany Serrato. Peirce allegories. identities involving transitive elements and symmetrical ones. Journal of Pure and Applied Algebra, 116(1-3):249-271, 1997. Google Scholar
  54. Charles S. Peirce. The logic of relatives. The Monist, 7(2):161-217, 1897. URL: http://www.jstor.org/stable/27897407.
  55. Charles Sanders Peirce. Studies in logic. By members of the Johns Hopkins university. Little, Brown, and Company, 1883. Google Scholar
  56. Robin Piedeleu and Fabio Zanasi. A String Diagrammatic Axiomatisation of Finite-State Automata. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, pages 469-489, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-71995-1_24.
  57. A.M. Pitts. Tripos theory in retrospect. Math. Struct. in Comp. Science, 12:265-279, 2002. Google Scholar
  58. Damien Pous. Kleene algebra with tests and coq tools for while programs. In Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings 4, pages 180-196. Springer, 2013. Google Scholar
  59. Damien Pous. Automata for relation algebra and formal proofs. PhD thesis, ENS Lyon, 2016. Google Scholar
  60. Damien Pous. On the positive calculus of relations with transitive closure. In Rolf Niedermeier and Brigitte Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France, volume 96 of LIPIcs, pages 3:1-3:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.3.
  61. Vaughan R Pratt. Semantical considerations on floyd-hoare logic. In 17th Annual Symposium on Foundations of Computer Science (sfcs 1976), pages 109-121. IEEE, 1976. Google Scholar
  62. W.V. Quine. Predicate-functor logics. In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 309-315. Elsevier, 1971. URL: https://doi.org/10.1016/S0049-237X(08)70850-4.
  63. Valentin N Redko. On defining relations for the algebra of regular events. Ukrainskii Matematicheskii Zhurnal, 16:120-126, 1964. Google Scholar
  64. Don D. Roberts. The Existential Graphs of Charles S. Peirce. De Gruyter Mouton, 1973. Google Scholar
  65. P. Selinger. A Survey of Graphical Languages for Monoidal Categories. In B. Coecke, editor, New Structures for Physics, volume 813 of Lecture Notes in Physics, pages 289-355. Springer, Berlin, Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
  66. Dario Stein and Sam Staton. Probabilistic programming with exact conditions. Journal of the ACM, 2023. Google Scholar
  67. Alfred Tarski. On the calculus of relations. The Journal of Symbolic Logic, 6(3):73-89, September 1941. URL: https://doi.org/10.2307/2268577.
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