Remarks on Elementary Linear Logic

Last works in linear logic mark a trend that can be summarized as: studying of fragments of calculi which have good logical properties and a quite powerful class of representable functions. ELL is a system derived from linear logic which presents several of such good properties: first of all a bound of the cut-elimination procedure which is lower w.r.t. the usual one. 1 Introduction Linear Logic provides a framework to study phenomena of non-linearity in logical calculi. Calculus properties usually studied regard the representability of functions (i.e. recursive functions) and properties of cut-elimination (i.e. its termination, confluence and complexity). The introduction of linear logic is primarily aimed at studying classical logic and as such it benefits from fragments in some way conservative of the above mentioned properties. It is clear that a purely linear fragment does not hold any expressive power in terms of functions, but it is also clear that full linear logic has some di..