Compositional Diagrammatic First-Order Logic
Nathan Haydon and Pawel Sobocinski
Peirceâ€™s Î² variant of Existential Graphs (EGs) is a diagrammatic formalism, equivalent in expressive power to classical first-order logic. We show that the syntax of EGs can be presented as the arrows of a free symmetric monoidal category. The advantages of this approach are (i) that the associated string diagrams share the visual features of EGs while (ii) enabling a rigorous distinction between â€œfreeâ€ and â€œboundâ€ variables. Indeed, this diagrammatic language leads to a compositional relationship of the syntax with the semantics of logic: we obtain models as structure-preserving monoidal functors to the category of relations. In addition to a diagrammatic syntax for formulas, Peirce developed a sound and complete system of diagrammatic reasoning that arose out of his study of the algebra of relations. Translated to string diagrams we show the implied algebraic structure of EGs sans negation is that of cartesian bicategories of relations: for example, lines of identity obey the laws of special Frobenius algebras. We also show how the algebra of negation can be presented, thus capturing Peirceâ€™s full calculus.