CUT ELIMINATION FOR CLASSICAL BILINEAR LOGIC
Jim Lambek · Fundamenta Informaticae · 1995
In this paper a cut elimination theorem is proved for classical non-commutative linear logic without exponentials, presented as a dual Schütte style deductive system. The notion of equality between deductions is sketched and they are interpreted as r