Abstract

Thirty years ago, I introduced a noncommutative variant of classical linear logic, called pomset logic, coming from a particular categorical interpretation of linear logic known as coherence spaces. In addition to the usual commutative multiplicative connectives of linear logic, pomset logic includes a noncommutative connective, “⊲” called before, associative and self-dual: ⊥ = A⊥ ⊲ B⊥. The conclusion of a pomset logic proof is a Partially Ordered Multiset of formulas. Pomset logic enjoys a proof net calculus with cut-elimination, denotational semantics, and faithfully embeds sequent calculus. The study of pomset logic has reopened with recent results on handsome proof nets, on its sequent calculus, or on its follow-up calculi like deep inference by Guglielmi and Straßburger. Therefore, it is high time we published a thorough presentation of pomset logic, including published and unpublished material, old and new results. Pomset logic is a noncommutative variant of linear logic as is Lambek calculus and it can also be used as a grammatical formalism. Those two calculi are quite different, but we hope that the algebraic presentation we give here, with formulas as algebraic terms and with a semantic notion of proof correctness, better matches Lambek’s view of what a logic should be.