23 April 2020, 14:00, online

Speaker

Jens Seeber, Scuola IMT Alti Studi Lucca

Title

Logical Completeness for String Diagrams

Abstract

String diagrams can be used as a compositional syntax for different kinds of computational structures. This thesis views string diagrams through a logical/universal algebraic perspective – diagrams represent formulas, allowing the use of diagrammatic reasoning for proofs. The category theoretic backdrop of this playground is given by the concept of Cartesian bicategory – a categorical algebra of relations – that we consider as a relational theory through the lens of functorial semantics. Given a Cartesian bicategory, functorial semantics provides us with an appropriate notion of model as a structure-preserving functor to the category of sets and relations.

Functoriality implies that diagrammatic reasoning is sound. The central question this approach raises and that we shall settle is the question of completeness in the logical sense: does every property that is shared by all models have a diagrammatic proof?

The answer to the above question is positive. To show this, we give a combinatorial characterisation of Cartesian bicategories in terms of hypergraphs equipped with interfaces, inspired by a seminal result by Chandra and Merlin. This reduces the problem of logical completeness to a categorical lifting problem that we solve using a transfinite construction and a compactness argument.