Specifying Proof Systems in Linear Logic with Subexponentials

AbstractIn the past years, linear logic has been successfully used as a general logical framework for encoding proof systems. Due to linear logicʼs finer control on structural rules, it is possible to match the structural restrictions specified in the encoded logic with the use of linear logic connectives. However, some systems that impose more complicated structural restrictions on its sequents cannot be easily captured in linear logic, since it only distinguishes two types of formulas: classical and linear. This work shows that one can encode a wider range of proof systems by using focused linear logic with subexponentials. We demonstrate this by encoding the system G1m for minimal, the multi-conclusion system, mLJ, and the focused system LJQ*, for intuitionistic logic. Finally, we identify general conditions for determining whether a linear logic formula corresponds to an object-logic rule and whether this rule is invertible