Proof nets for the multimodal Lambek Calculus

Abstract

Since the introduction of proof nets as an elegant proof theory for the multiplicative fragment of linear logic in Girard a number of attempts have been made to adapt this proof theory to a variety of Lambek Calculi as shown by work from eg Roorda Morrill and Moortgat In this paper we will present a new way to look at proof nets for the multimodal Lambek Calculus We will show how we can uniformly handle both the unary and the binary connectives and how we have a natural correctness criterion for the base logic NL together with a set R of structural rules subject to a linearity condition First we introduce proof structures for our calculus Following Puite we will allow proof structures to have hypotheses in addition to conclusions Then we will look at slightly more abstract graphs which we will call hypothesis structures on which we will formulate a correctness criterion in the form of graph conversions Proof nets will be those proof structures of which the hypothesis structure converts to a tree