!-Logic

Equational reasoning with string diagrams provides an intuitive method for proving equations between morphisms in various forms of monoidal category. !-Graphs were introduced with the intention of reasoning with infinite families of string diagrams by allowing repetition of sub-diagrams. However, their combinatoric nature only allows commutative nodes. The aim of this thesis is to extend the !-graph formalism to remove the restriction of commutativity and replace the notion of equational reasoning with a natural deduction system based on first order logic. The first major contribution is the syntactic !-tensor formalism, which enriches Penrose’s abstract tensor notation to allow repeated structure via !-boxes. This will allow us to work with many noncommutative theories such as bialgebras, Frobenius algebras, and Hopf algebras, which have applications in quantum information theory. A more subtle consequence of switching to !-tensors is the ability to definitionally extend a theory. We will demonstrate how noncommutativity allows us to define nodes which encapsulate entire diagrams, without inherently assuming the diagram is commutative. This is particularly useful for recursively defining arbitrary arity nodes from fixed arity nodes. For example, we can construct a !-tensor node representing the family of left associated trees of multiplications in a monoid. The ability to recursively define nodes goes hand in hand with proof by induction. This leads to the second major contribution of this thesis, which is !-Logic (!L). We extend previous attempts at equational reasoning to a fully fledged natural deduction system based on positive intuitionistic first order logic, with conjunction, implication, and universal quantification over !-boxes. The key component of !L is the principle of !-box induction. We demonstrate its application by proving how we can transition from fixed to arbitrary arity theories for monoids, antihomomorphisms, bialgebras, and various forms of Frobenius algebras. We also define a semantics for !L, which we use to prove its soundness. Finally, we reintroduce commutativity as an optional property of a morphism, along with another property called symmetry, which describes morphisms which are not affected by cyclic permutations of their edges. Implementing these notions in the !-tensor language allows us to more easily describe theories involving symmetric or commutative morphisms, which we then demonstrate for recursively defined Frobenius algebra nodes.