Graphical Regular Logic
Brendan Fong, David I Spivak

TL;DR
This paper develops a graphical string diagram calculus for regular logic, connecting regular theories with monoidal 2-functors and demonstrating the reflective relationship between regular categories and regular calculi.
Contribution
It introduces a categorical framework for regular logic using graphical calculus and establishes the reflectiveness of regular categories within regular calculi.
Findings
Graphical string diagram calculus for regular logic
Regular theories as monoidal 2-functors to posets
Reflective relationship between regular categories and calculi
Abstract
Regular logic can be regarded as the internal language of regular categories, but the logic itself is generally not given a categorical treatment. In this paper, we understand the syntax and proof rules of regular logic in terms of the free regular category on a set . From this point of view, regular theories are certain monoidal 2-functors from a suitable 2-category of contexts---the 2-category of relations in ---to the 2-category of posets. Such functors assign to each context the set of formulas in that context, ordered by entailment. We refer to such a 2-functor as a regular calculus because it naturally gives rise to a graphical string diagram calculus in the spirit of Joyal and Street. Our key aim to prove that the category of regular categories is essentially reflective in that of regular calculi. Along the way, we…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Homotopy and Cohomology in Algebraic Topology · Logic, Reasoning, and Knowledge
