System NEL is Undecidable

Abstract

System NEL is a conservative extension of multiplicative exponential linear logic (extended by the rules mix and nullary mix) by a self-dual noncommutative connective called seq which has an intermediate position between the connectives par and times. In this paper, I will show that system NEL is undecidable by encoding two counter machines into NEL. Although the encoding is simple, the proof of the faithfulness is a little intricate because there is no sequent calculus and no phase semantics available for NEL.