eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
171
189
10.4230/LIPIcs.CALCO.2015.171
article
A First-order Logic for String Diagrams
Kissinger, Aleks
Quick, David
Equational reasoning with string diagrams provides an intuitive means of proving equations between morphisms in a symmetric monoidal category. This can be extended to proofs of infinite families of equations using a simple graphical syntax called !-box notation. While this does greatly increase the proving power of string diagrams, previous attempts to go beyond equational reasoning have been largely ad hoc, owing to the lack of a suitable logical framework for diagrammatic proofs involving !-boxes. In this paper, we extend equational reasoning with !-boxes to a fully-fledged first order logic with conjunction, implication, and universal quantification over !-boxes. This logic, called !L, is then rich enough to properly formalise an induction principle for !-boxes. We then build a standard model for !L and give an example proof of a theorem for non-commutative bialgebras using !L, which is unobtainable by equational reasoning alone.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.171/LIPIcs.CALCO.2015.171.pdf
string diagrams
compact closed monoidal categories
abstract tensor systems
first-order logic