The decidability of the intensional fragment of classical linear logic (Q2517231): Difference between revisions

The linear logic by Girard is one of the most interesting substructural logics. In the setting of sequent calculus, one can easily observe its peculiar features like having two kinds of conjunction and disjunction and controlled application of structural rules (weakening, contraction) restricted to some modalised formulas. Although it is known that full propositional linear logic is not decidable it does not preclude the possibility of having its decidable fragments. In the paper, the intensional fragment is examined with two-premiss context-free rules (multiplicative conjunction and disjunction) and it is shown to be decidable. Moreover, the same results are provided for some related logic called intensional interlinear logic, where unrestricted contraction is added. In the last section, it is also shown how to extend these results to intuitionistic versions of both logics and to versions with added so called Ackermann's constants. The main result (i.e. decidability) is proved for sequent calculi of the abovementioned logics. In both cases, two formalizations are provided; in the latter (the controlled) contraction rules are dropped but the effect of their application is absorbed into other rules. For all calculi, the admissibility of cut (or contraction-absorbing cut) is proved. In case of the first calculus (with explicit contraction rules) except degree and rank of cut-formula, also the number of contraction applications is taken as an additional induction parameter. In Section 4, a decidability is proved on the basis of modified Curry's lemma and Kripke's lemma. The paper is dense but readable. The presented results are important and may serve as an interesting illustration of the application of methods previously applied by the author to other nonclassical logics. For further information, the reader should consult [Proof theory. Sequent calculi and related formalisms. Boca Raton, FL: CRC Press (2015; Zbl 1302.03001)] by the same author.