Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1016/j.apal.2016.10.008 | Annals of Pure and Applied Logic |
Keywords | Field | DocType |
03F52,18A15,18D10,18D15 | Intuitionistic logic,Discrete mathematics,Autoepistemic logic,Algebra,Paraconsistent logic,Multimodal logic,Substructural logic,Predicate functor logic,Many-valued logic,Mathematics,Intermediate logic | Journal |
Volume | Issue | ISSN |
168 | 2 | 0168-0072 |
Citations | PageRank | References |
0 | 0.34 | 2 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Paul-andré Melliès | 1 | 392 | 30.70 |