In this paper we investigate the notion of generalized connective for multiplicative linear logic. We introduce a notion of orthogonality for partitions of a finite set and we study the family of connectives which can be described by two orthogonal sets of partitions. We prove that there is a special class of connectives that can never be decomposed by means of the multiplicative conjunction ⊗ and disjunction ⅋, providing an infinite family of non-decomposable connectives, called Girard connectives. We show that each Girard connective can be naturally described by a type (a set of partitions equal to its double-orthogonal) and its orthogonal type. In addition, one of these two types is the union of the types associated to a family of MLL-formulas in disjunctive normal form, and these formulas only differ for the cyclic permutations of their atoms.

Abstract This paper presents a simple and intuitive syntax for proof nets of the multiplicative cyclic fragment (McyLL) of linear logic (LL). The main technical achievement of this work is to propose a correctness criterion that allows for sequentialization (recovering a proof from a proof net) for all McyLL proof nets, including those containing cut links. This is achieved by adapting the idea of contractibility (originally introduced by Danos to give a quadratic time procedure for proof nets correctness) to cyclic LL. This paper also gives a characterization of McyLL proof nets for Lambek Calculus and thus a geometrical (i.e., non-inductive) way to parse phrases or sentences by means of Lambek proof nets.

We present a syntax for MALL (multiplicative additive linear logic without units) proof nets which refines Girard's one. It is also based on the use of monomial weights for identifying additive components (slices). Our generalization gives the possibility of representing a kind of sharing of nodes which does not exist in Girard's nets. This sharing leads to the definition of a strong cut elimination procedure for MALL. We give a correctness criterion which is proved to be stable by reduction and to give a sequentialization theorem with respect to the sequent calculus. Sequentialization is proved by showing that an expansion procedure allows us to unfold any of our proof nets into a Girard proof net.