View Related Documents

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 P{\it \Pi} of second order mELL that cannot have a representative P¢{\it \Pi'} 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.

Fulltext Preview

Image of the first page of the fulltext document