Specifying Proof Systems in Linear Logic with Subexponentials

In 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 multiconclusion system, mLJ, and the focused system LJQ∗ , for intuitionistic logic. Finally, we identify general conditions for determining whether a linear logic formula corresponds to a object-logic rule and whether this rule is invertible.

• Type: Journal
• Year: 2011
• Where: ENTCS
• Authors: Vivek Nigam, Elaine Pimentel, Giselle Reis
• Keywords: ENTCS 2011, Linear Logic, Linear Logic Connectives, Structural Restrictions