A by-level analysis of multiplicative exponential linear logic

Abstract

We study the relations between Multiplicative Exponential Linear Logic (mELL) and Baillot-Mazza Linear Logic by Levels (mL 3). We design a decoration-based translation between propositional mELL and propositional mL 3. The translation preserves the cut elimination. Moreover, we show that there is a proof net of second order mELL that cannot have a representative ∏ ′ in second order mL 3 under any decoration. This suggests that levels can be an analytical tool in understanding the complexity of second order quantifier. © 2009 Springer Berlin Heidelberg.