Document Open Access Logo

Functorial Semantics for First-Order Theories

Authors Filippo Bonchi , Alessandro Di Giorgio , Roberto Di Virgilio , Paweł Sobociński

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2026.44.pdf
  • Filesize: 0.92 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • First-order logic
  • Model theory
  • Functorial semantics
  • String diagrams

Metrics

Abstract

Building on the recent axiomatisation of first-order bicategories, we develop a functorial semantics approach to the model theory of first-order logic. First-order theories 𝕋 are captured by free first-order bicategories ℱ_𝕋 and models of𝕋 are structure-preserving functors from ℱ_𝕋 to a first-order bicategory 𝐂. Elementary morphisms of models arise as lax natural transformations between such functors, and the classical Tarski-Vaught test and downward Löwenheim-Skolem theorem admit direct diagrammatic proofs. Our results instantiate classically when 𝐂 = Rel and hold uniformly for models valued in Rel(𝐃) over an arbitrary Boolean geometric category 𝐃 in which regular epis split.

Cite As Get BibTex

Filippo Bonchi, Alessandro Di Giorgio, Roberto Di Virgilio, and Paweł Sobociński. Functorial Semantics for First-Order Theories. In 51st International Symposium on Mathematical Foundations of Computer Science (MFCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 386, pp. 44:1-44:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.MFCS.2026.44

Author Details

Filippo Bonchi
  • Università di Pisa, Italy
Alessandro Di Giorgio
  • Tallinn University of Technology, Estonia
Roberto Di Virgilio
  • Tallinn University of Technology, Estonia
Paweł Sobociński
  • Tallinn University of Technology, Estonia

Funding

Di Virgilio and Sobociński were supported by the Estonian Research Council via grant PRG3215. Di Giorgio and Sobociński were supported by the European Union under Grant Agreement No. 101087529. Bonchi and Sobociński were supported by the ARIA UK Safeguarded AI programme. Sobociński was additionally supported by the Estonian Research Council via grant TEM-TA5 and the Estonian Center of Excellence in Artificial Intelligence (EXAI).

Acknowledgements

The authors would like to thank the anonymous reviewers of MFCS 2026 for providing a simpler proof of Lemma 24 and for spotting and fixing errors in Section 6.

References

  1. Jiří Adámek and Jiří Rosický. Locally Presentable and Accessible Categories, volume 189 of London Mathematical Society Lecture Note Series. CUP, 1994. URL: https://doi.org/10.1017/CBO9780511600579.
  2. Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: an online proof assistant for higher-dimensional rewriting. Logical Methods in Computer Science, 14, 2018. URL: https://doi.org/10.23638/LMCS-14(1:8)2018.
  3. Filippo Bonchi, Alessandro Di Giorgio, and Alessio Santamaria. Deconstructing the calculus of relations with tape diagrams. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571257.
  4. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobociński, 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, Nathan Haydon, and Paweł Sobociński. Diagrammatic algebra of first order logic. In Paweł Sobociński, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 16:1-16:15. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662078.
  6. Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta. When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines. In Rastislav Královic and Antonín Kucera, editors, 49th International Symposium on Mathematical Foundations of Computer Science, MFCS 2024, August 26-30, 2024, Bratislava, Slovakia, volume 306 of LIPIcs, pages 30:1-30:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.MFCS.2024.30.
  7. Filippo Bonchi, Dusko Pavlovic, and Paweł Sobociński. Functorial semantics for relational theories. Polynesian Journal of Mathematics, 2(6):1-56, October 2025. URL: https://doi.org/10.69763/polyjmath.2.6.
  8. 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. URL: https://doi.org/10.4230/LIPIcs.CALCO.2021.10.
  9. Filippo Bonchi, Jens Seeber, and Paweł Sobociński. Graphical Conjunctive Queries. In Dan Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 of LIPIcs, pages 13:1-13:23, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.13.
  10. Filippo Bonchi, Jens Seeber, and Paweł Sobociński. The Axiom of Choice in Cartesian Bicategories. In Markus Roggenbach and Ana Sokolova, editors, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019), volume 139 of LIPIcs, pages 15:1-15:17, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CALCO.2019.15.
  11. Francis Borceux. Handbook of Categorical Algebra 2 - Categories and Structures. CUP, 1994. URL: https://doi.org/10.1017/CBO9780511525865.
  12. 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.
  13. Luc Chabassier. A graphical interface for category theory proofs in Coq. In Theorem Proving Components for Educational Software 2024 (ThEdu’24), volume 419 of EPTCS, pages 28-41, 2025. URL: https://doi.org/10.4204/EPTCS.419.2.
  14. Ashok K. Chandra and Philip M. Merlin. Optimal implementation of conjunctive queries in relational data bases. In Proceedings of the Ninth Annual ACM Symposium on Theory of Computing, STOC '77, pages 77-90, New York, NY, USA, May 1977. Association for Computing Machinery. URL: https://doi.org/10.1145/800105.803397.
  15. 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. URL: https://doi.org/10.1017/S0960129520003047.
  16. Bob Coecke and Ross Duncan. Interacting Quantum Observables. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Automata, Languages and Programming, Lecture Notes in Computer Science, pages 298-310, Berlin, Heidelberg, 2008. Springer. URL: https://doi.org/10.1007/978-3-540-70583-3_25.
  17. Andrea Corradini, Ugo Montanari, Francesca Rossi, Hartmut Ehrig, Reiko Heckel, Michael Löwe, et al. Algebraic approaches to graph transformation-part I: Basic concepts and double pushout approach, 1997. URL: https://doi.org/10.5555/278918.278928.
  18. Alessandro Di Giorgio. Diagrammatic Algebras of Relations. PhD thesis, Università di Pisa, 2024. Google Scholar
  19. Ivan Di Liberti, Fosco Loregiàn, Chad Nester, and Paweł Sobociński. Functorial semantics for partial theories. Proc. ACM Program. Lang., 5(POPL):1-28, 2021. URL: https://doi.org/10.1145/3434338.
  20. Radu Diaconescu. Axiom of choice and complementation. Proceedings of the American Mathematical Society, 51(1):176-178, 1975. URL: https://doi.org/10.1090/S0002-9939-1975-0373893-X.
  21. Sam Ezeh. Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4 (short paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024), pages 41-1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.41.
  22. Brendan Fong and David I Spivak. Regular and relational categories: Revisiting `Cartesian bicategories I'. arXiv preprint arXiv:1909.00069, 2019. URL: https://doi.org/10.48550/arXiv.1909.00069.
  23. Peter Freyd and Andre Scedrov. Categories, Allegories, volume 39 of North-Holland Mathematical Library. Elsevier B.V, 1990. URL: https://doi.org/10.2307/2275344.
  24. Nathan Haydon and Paweł Sobociński. Compositional diagrammatic first-order logic. In Ahti-Veikko Pietarinen, Peter Chapman, Leonie Bosveld-de Smet, Valeria Giardino, James E. Corter, and Sven Linker, editors, Diagrammatic Representation and Inference - 11th International Conference, Diagrams 2020, Tallinn, Estonia, August 24-28, 2020, Proceedings, LNCS, pages 402-418. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-54249-8_32.
  25. Bart Jacobs. Categorical logic and type theory, volume 141. Elsevier, 1999. URL: https://doi.org/10.1016/s0049-237x(98)x8028-6.
  26. Niles Johnson and Donald Yau. Bimonoidal Categories, E_n-Monoidal Categories, and Algebraic K-Theory: Volume III: From Categories to Structured Ring Spectra, volume 285. American Mathematical Society, 2024. URL: https://doi.org/10.1090/surv/285.
  27. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium, Volume 1, volume 43 of Oxford Logic Guides. OUP, 2002. URL: https://doi.org/10.1017/S1079898600003462.
  28. 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.
  29. Aleks Kissinger. Chyp, 2023. URL: https://github.com/akissinger/chyp.
  30. Aleks Kissinger and Vladimir Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 326-336, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-21401-6_22.
  31. 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.
  32. Stephen Lack. Composing PROPs. Theory and Application of Categories, 13(9):147-163, 2004. Google Scholar
  33. F. W. Lawvere. Functorial Semantics of Algebraic Theories. PhD thesis, Columbia University, New York, NY, USA, 1963. Google Scholar
  34. F William Lawvere. Adjointness in foundations. Dialectica, pages 281-296, 1969. URL: https://doi.org/10.1111/j.1746-8361.1969.tb01194.x.
  35. Adrian Lehmann, Ben Caldwell, Bhakti Shah, William Spencer, and Robert Rand. VyZX: Formal verification of a graphical quantum language. ACM Transactions on Programming Languages and Systems, 2026. URL: https://doi.org/10.1145/3807780.
  36. Leopold Löwenheim. Über möglichkeiten im relativkalkül. Mathematische Annalen, 76:447-470, 1915. URL: https://doi.org/10.1007/BF01458217.
  37. S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, second edition, 1978. URL: https://doi.org/10.1007/978-1-4757-4721-8.
  38. Michael Makkai and Gonzalo E Reyes. First order categorical logic: model-theoretical methods in the theory of topoi and related categories. Springer, 2006. URL: https://doi.org/10.1007/BFb0066201.
  39. 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. URL: https://doi.org/10.1145/2933575.2934525.
  40. Charles S. Peirce. The logic of relatives. The Monist, 7(2):161-217, 1897. URL: https://doi.org/10.5840/monist18977231.
  41. Andrew M Pitts. Categorical logic. Handbook of logic in computer science, 5:39-128, 2001. URL: https://doi.org/10.1093/oso/9780198537816.003.0002.
  42. 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. URL: https://doi.org/10.1007/978-3-642-39634-2_15.
  43. Damien Pous. Automata for relation algebra and formal proofs. PhD thesis, ENS Lyon, 2016. Google Scholar
  44. 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.
  45. Damien Pous. String diagrams for monoidal categories, in Rocq. CoRR, abs/2602.19806, 2026. URL: https://doi.org/10.48550/arXiv.2602.19806.
  46. Arend Rensink and Andrea Corradini. On categories of nested conditions. In Nils Jansen, Sebastian Junges, Benjamin Lucien Kaminski, Christoph Matheja, Thomas Noll, Tim Quatmann, Mariëlle Stoelinga, and Matthias Volk, editors, Principles of Verification: Cycling the Probabilistic Landscape - Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part I, volume 15260 of LNCS, pages 393-418. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-75783-9_16.
  47. Peter Selinger. A survey of graphical languages for monoidal categories. In New structures for physics, pages 289-355. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12821-9_4.
  48. Bhakti Shah, Willam Spencer, Laura Zielinski, Ben Caldwell, Adrian Lehmann, and Robert Rand. ViCAR: Visualizing categories with automated rewriting in Coq. In Applied Category Theory 2024, volume 429 of EPTCS, pages 234-248, 2024. URL: https://doi.org/10.4204/EPTCS.429.13.
  49. 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.
  50. Alfred Tarski and Steven R Givant. A formalization of set theory without variables, volume 41. American Mathematical Soc., 1988. URL: https://doi.org/10.1090/coll/041.
  51. Alfred Tarski and Robert L. Vaught. Arithmetical extensions of relational systems. Compositio Mathematica, 13:81-102, 1957. URL: https://doi.org/10.2307/2271293.
  52. Sam van Gool and Jérémie Marquès. On duality and model theory for polyadic spaces. Annals of Pure and Applied Logic, 175(2):103388, 2024. URL: https://doi.org/10.1016/j.apal.2023.103388.
  53. I Ben Yaacov, Alexander Berenstein, C Ward Henson, and Alexander Usvyatsov. Model theory for metric structures. London Mathematical Society Lecture Note Series, 350:315, 2008. URL: https://doi.org/10.1017/CBO9780511735219.011.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact