Introduction

The aim of this paper is to give a purely graph-theoretical definition of noncommutative proof nets, i.e. graphs coming from proofs in MNLL (multiplicative noncommutative linear logic, the (⊗, ℘)-fragment of the one-sided sequent calculus for classical noncommutative linear logic, introduced in [Abr91]). Analogously, one of the aims of [Gir87] was to give a purely graph-theoretical definition of proof nets, i.e. graphs coming from the proofs in MLL (multiplicative linear logic, the (⊗, ℘)-fragment of the one-sided sequent calculus for classical linear logic - better, for classical commutative linear logic). - The relevance of the purely graph-theoretical definition of proof nets for the development of commutative linear logic is well-know; thus we hope the results of this paper will be useful for a similar development of noncommutative linear logic.

The language for MNLL is an extension of the language for MLL, obtained simply adding, as atomic formulas, propositional letters with an arbitrary finite number of negations written after the propositional letter (linear post-negation) or before the propositional letter (linear retronegation). Every formula A of MNLL may be translated into a formula Tv(A) of MLL (simply by replacing each propositional letter with an even number of negations by the propositional letter without negations, and each propositional letter with an odd number of negations by the propositional letter with only one negation after the propositional letter).