Topic Archive: Linear Logic
Linear Logic, introduced by Girard ([Gir] 1987), is a kind of resource sensitive logic, since it lacks general forms of structural inferences. However, it restores controlled uses of structural inferences by its exponentials, which behaves like the S4 modality. In the usual resource semantics for Linear Logic, the formulas with exponentials are interpreted to mean the inexhaustibility of a resource. We study an extension of Linear Logic by relaxing the exponentials to the S5 type modality. Then, it is interpreted to mean the inexhaustibility and transferability of a resource. We show some basic properties of this logic: completeness, cut-eliminatbility, decidability. Also, we provide the realizability of our logic via Logic of proofs (aka, Justification Logic), introduced by Artemov [Art1, Art2].
This work is a continuation of our on-going research project with Professor Kurokawa on ’synthesizing substructural logics and logics of proofs’, including [KK], 2013.
[Art1] S. N. Artemov, Explicit provability and constructive semantics, Bulletin of Symbolic Logic 7(1), pp.1–36, 2001.
[Art2] S. N. Artemov, The Logic of Justification, Review of Symbolic Logic, 1(4), pp. 477-513, 2008.
[Gir] J. Girard, Linear Logic, Theoretical Computer Science 50, pp. 1–102, 1987.
[KK] H. Kurokawa and H. Kushida, Substructural Logic of Proofs, WoLLIC 2013: Logic, Language, Information, and Computation, LNCS 8071, pp.194-210, 2013.