Classical Linear Logic of Implications

Abstract. We give a simple term calculus for the multiplicative exponential fragment of Classical Linear Logic, by extending Barber and Plotkin's system for the intuitionistic case. The calculus has the nonlinear and linear implications as the basic constructs, and this design choice allows a technically managable axiomatization without commuting conversions. Despite this simplicity, the calculus is shown to be sound and complete for category-theoretic models given by -autonomous categories with linear exponential comonads.

• Type: Journal
• Year: 2002
• Where: CSL
• Authors: Masahito Hasegawa
• Keywords: Automated Reasoning, Classical Linear Logic, CSL 2002, Multiplicative Exponential Fragment, Simple Term Calculus