×

zbMATH — the first resource for mathematics

Quantales and (noncommutative) linear logic. (English) Zbl 0701.03026
Girard’s linear logic is essentially classical predicate logic without contraction and weakening rules but with S4-modality !, for which all antecedent structural rules are postulated. Noncommutative Linear Logic NLL is obtained by dropping the permutation rule. Systems of this kind for the connectives \(\otimes\) (tensor product) and \(\to\) (inner Hom- functor) were introduced and investigated by Lambek and MacLane in connection with problems in category theory. With reference to Girard’s unpublished lectures the author considers pure succeedent sequent calculus for NLL, where the main (i.e. analysed) formula is always the leftmost one. Then the form of the \(\otimes\)-rule: A,\(\phi\) ;B,\(\psi\) /(A\(\otimes B),\Psi,\Phi\) with exactly these positions of the formula lists \(\Phi\), \(\Psi\) is essential. Equivalence to Lambek’s previous formulation for the (\(\otimes,\to)\) language is achieved by postulating the cyclic substitution rule \(\Phi\) /\(\Psi\), where formula list \(\Psi\) is a cyclic substitution of \(\Phi\). [One of the reasons of considering NLL given by Lambek was the unrestricted coherence theorem for closed categories, which in proof-theoretic terms can be formulated as follows: if every propositional variable occurs exactly twice in a given sequent S, then S has at most one derivation modulo standard cut-elimination steps. The author does not mention this, probably because additional introduction of the connectives \(\wedge\), \(\vee\) (cartesian product and its dual) destroys coherence: the formula ((a\(\wedge b)\otimes ((a\vee b)\to c))\to c\) has two different derivations depending on the choice of the conjuncts a, b.] For the noncommutative case the author postulates all antecedent structural rules for !-formulas but drops !-introduction into antecedent, which makes ! a K4-modality. Besides that, a new modality k is introduced for which S4-rules, permutation and the relation kA\(\to \neg !\neg A\) are postulated. It is noted that Girard’s translation of intuitionistic predicate logic into linear logic (transforming \(A\supset B\) into !A\(\to B\), \(A\vee B\) into !A\(\vee !B\) and leaving the remaining connectives unchanged) is sound and faithful also for NLL. Faithful embedding of commutative linear logic into NLL is achieved by prefixing k to all subformulas which do not begin with !. The quantale mentioned in the title is a complete lattice (Q,V) enriched with the associative tensor product \(\otimes\), which distributes on both sides over arbitrary \(\vee\). This kind of models was considered in quantum logic [S. Niefield and K. Rosenthal, Math. Proc. Camb. Philos. Soc. 104, 215-234 (1988; Zbl 0658.06007)]. Implication (left and right one) is defined there in a natural way. Completeness theorem is established for Girard quantales with element \(\perp\) satisfying dualization conditions \((a\to \perp)\to \perp =a\) for both implications, and cyclicity \(a\to \neg b=b\to \neg a\), provided modalities satisfying appropriate conditions are also present. This part of the material is rather traditional. More interesting is the notion of (proof as) drawing, which the author proposes instead of Girard’s proof-nets. A drawing is a labelled topological structure on some surface. Every sequent derivation is translated into a drawing. It is asserted that correctness of a drawing can be recognized in one pass, while testing correctness of a proof-net is exponential. A graphical proof is defined as equivalence class of drawings under orientation-preserving diffeomorphisms of the underlying surfaces, and some additional transformations. A very short outline of the proof of strong normalization for graphical proofs is presented. It is stated that this work is connected with results of the author and P. Freyd on coherence theorems and low dimensional topology. Unfortunately the definitions in this part of the paper are only sketched, and proofs are practically absent. It would be interesting to know whether the coherence theorem is true for the commutative (\(\otimes,\to,!)\)-language and the noncommutative (\(\otimes,\to,\perp,!)\)-language, respectively.
Reviewer: G.Mints

MSC:
03F05 Cut-elimination and normal-form theorems
18A15 Foundations, relations to logic and deductive systems
03B45 Modal logic (including the logic of norms)
03G30 Categorical logic, topoi
06B23 Complete lattices, completions
06F05 Ordered semigroups and monoids
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] DOI: 10.1016/0304-3975(87)90045-4 · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4
[2] Advances in Mathematics
[3] DOI: 10.2307/1968621 · Zbl 0015.14603 · doi:10.2307/1968621
[4] DOI: 10.1063/1.522736 · doi:10.1063/1.522736
[5] Seminar lectures, Le Groupe Interuniversitaire en Études Catégoriques (1987)
[6] Computational problems in abstract algebra pp 263– (1970) · doi:10.1016/B978-0-08-012975-4.50028-X
[7] DOI: 10.1017/S0305004100065403 · Zbl 0658.06007 · doi:10.1017/S0305004100065403
[8] Logico-algebraic approach to quantum mechanics II (1979)
[9] Second topology conference (Taormina, 1984), Rendiconti del Circolo Matematico di Palermo pp 94– (1986)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.