Non-commutative logic II: sequent calculus and phase semantics

Non-commutative logic, which is an unification of commutative linear logic and cyclic linear logic, is extended to all linear connectives: additives, exponentials and constants. We give two equivalent versions of the sequent calculus --- directly with the structure of series-parallel order varieties, and with their presentations as partial orders ---, phase semantics and a cut elimination theorem. Contents 1 Introduction 2 2 Sequent calculus : first version 5 2.1 Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3 Order varieties 12 3.1 Order varieties and orders . . . . . . . . . . . . . . . . . . . . 12 3.2 Series-parallel order varieties . . . . . . . . . . . . . . . . . . 14 3.3 Characterization of series-parallel order varieties . . . . . . . 16 Post-doctoral fellowship from the INRIA. This research was pa..