×

Proof theory for full intuitionistic linear logic, bilinear logic, and MIX categories. (English) Zbl 0879.03022

The paper is part of a series of papers on the structure of linearly distributive categories (the notion corresponds to the “weakly distributive categories” in the papers written earlier [e.g., R. F. Blute, J. R. B. Cockett and R. A. G. Seely, “Categories for computation in context and unified logic”, J. Pure Appl. Algebra 116, 49-98 (1997); see the review above]. The notion of linearly distributive category was introduced to study the cut rule in the sequent calculus with finite sequences of formulas on both sides of turnstile. This proof theory is not truly “classical”, but may be thought of as the tensor-par fragement of linear logic with no negation. The logics considered in the paper are “Grishin Implicative Linear Logic” (GILL), “Full Intuitionistic Linear Logic” (FILL) of de Paiva and Hyland, and Lambek’s system BL2 or BILL. The principal difference of BILL and GILL from FILL is that the par-tensorial strength for the internal hom that arises from the linear distributivity should be an isomorphism. It is known that cut-elimination in FILL poses problems (Schellinx). The authors show, that when the derivations are presented in natural deduction style, these obstructions untangle in a rather natural way. The notion of “nucleus” of a commutative FILL category is studied, in connection with the notion of MIX rule for linearly distributive categories. It is shown that a linearly distributive category satisfies the MIX rule if its nucleus does. As a consequence, all linearly distributive categories which have either the tensor cartesian or par cartesian, necessarily satisfy the MIX rule.

MSC:

03G30 Categorical logic, topoi
03F05 Cut-elimination and normal-form theorems
03F07 Structure of proofs
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
PDFBibTeX XMLCite
Full Text: EuDML EMIS