A first-order logic for string diagrams

TL;DR

This paper introduces a first-order logic called !L for string diagrams with !-boxes, enabling formal proofs and induction principles that surpass previous ad hoc methods in diagrammatic reasoning.

Contribution

It extends equational reasoning with !-boxes to a comprehensive first-order logic, formalising induction and providing a standard model for diagrammatic proofs.

Findings

Developed !L, a first-order logic for string diagrams with !-boxes.

Formalised an induction principle for !-boxes within !L.

Proved a theorem for non-commutative bialgebras using !L.

Abstract

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 called 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.