A by-level analysis of Multiplicative Exponential Linear Logic

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.