We introduce a graphical language for closed symmetric monoidal categories based on an extension of string diagrams with special bracket wires representing internal homs. These bracket wires make the structure of the internal hom functor explicit, allowing standard morphism wires to interact with them through a well-defined set of graphical rules. We establish the soundness and completeness of the diagrammatic calculus, and illustrate its expressiveness through examples drawn from category theory, logic and programming language semantics.

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.

The calculus of relations was introduced by De Morgan and Peirce during the second half of the 19th century, as an extension of Boole's algebra of classes. Later developments on quantification theory by Frege and Peirce himself, paved the way to what is known today as first-order logic, causing the calculus of relations to be long forgotten. This was until 1941, when Tarski raised the question on the existence of a complete axiomatisation for it. This question found only negative answers: there is no finite axiomatisation for the calculus of relations and many of its fragments, as shown later by several no-go theorems. In this paper we show that -- by moving from traditional syntax (cartesian) to a diagrammatic one (monoidal) -- it is possible to have complete axiomatisations for the full calculus. The no-go theorems are circumvented by the fact that our calculus, named the calculus of neo-Peircean relations, is more expressive than the calculus of relations and, actually, as expressive as first-order logic. The axioms are obtained by combining two well known categorical structures: cartesian and linear bicategories. arXiv admin note: substantial text overlap with arXiv:2401.07055

Tape diagrams provide a graphical representation for arrows of rig categories, namely categories equipped with two monoidal structures, ⊕ and ⊗, where ⊗ distributes over ⊕. However, their applicability is limited to categories where ⊕ is a biproduct, i.e., both a categorical product and a coproduct. In this work, we extend tape diagrams to deal with Kleisli categories of symmetric monoidal monads, presented by algebraic theories.

Abstract Tape diagrams provide a convenient graphical notation for arrows of rig categories, i.e., categories equipped with two monoidal products, $$\oplus $$ ⊕ and $$\otimes $$ ⊗ . In this work, we introduce Kleene-Cartesian rig categories, namely rig categories where $$\otimes $$ ⊗ provides a Cartesian bicategory, while $$\oplus $$ ⊕ a Kleene bicategory.We show that the associated tape diagrams can conveniently deal with Hoare logic.

We introduce the calculus of neo-Peircean relations, a string diagrammatic extension of the calculus of binary relations that has the same expressivity as first order logic and comes with a complete axiomatisation. The axioms are obtained by combining two well known categorical structures: cartesian and linear bicategories.

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.

Rig categories with finite biproducts are categories with two monoidal products, where one is a biproduct and the other distributes over it. In this work we present tape diagrams, a sound and complete diagrammatic language for these categories, that can be intuitively thought as string diagrams of string diagrams. We test the effectiveness of our approach against the positive fragment of Tarski's calculus of relations.

Farkas' lemma is a celebrated result on the solutions of systems of linear inequalities, which finds application pervasively in mathematics and computer science. In this work we show how to formulate and prove Farkas' lemma in diagrammatic polyhedral algebra, a sound and complete graphical calculus for polyhedra. Furthermore, we show how linear programs can be modeled within the calculus and how some famous duality results can be proved.