A micrological study of negation

Tensorial logic is a primitive logic of tensor and negation which refines linear logic by relaxing the hypothesis that linear negation is involutive. Thanks to this mild modification, tensorial logic provides a type-theoretic account of game semantics where innocent strategies are portrayed as temporal refinements of traditional proof-nets in linear logic. In this paper, we study the algebraic and combinatorial structure of negation in a non-commutative variant of tensorial logic. The analysis is based on a 2-categorical account of dialogue categories, which unifies tensorial logic with linear logic, and discloses a primitive symmetry between proofs and anti-proofs. The micrological analysis of tensorial negation reveals that it can be decomposed into a series of more elementary components: an adjunction L⊣R between the left and right negation functors L and R; a pair of linear distributivity laws κ and κ which refines the linear distributivity law between ⊗ and ⅋ in linear logic, and generates the Opponent and Proponent views of innocent strategies between dialogue games; a pair of axiom and cut combinators adapted from linear logic; an involutive change of frame (−)⁎ reversing the point of view of Prover and of Denier on the logical dispute, and reversing the polarity of moves in the dialogue game associated to the tensorial formula.