TY - JOUR AU - Braüner, Torben AU - de Paiva, Valeria PY - 1996/01/10 Y2 - 2024/03/28 TI - Cut-Elimination for Full Intuitionistic Linear Logic JF - BRICS Report Series JA - BRICS VL - 3 IS - 10 SE - Articles DO - 10.7146/brics.v3i10.19973 UR - https://tidsskrift.dk/brics/article/view/19973 SP - AB - We describe in full detail a solution to the problem of proving the cut elimination theorem for FILL, a variant of (multiplicative and exponential-free) Linear Logic<br />introduced by Hyland and de Paiva. Hyland and de Paiva's work used a term assignment<br />system to describe FILL and barely sketched the proof of cut elimination. In this paper, as well as correcting a small mistake in their paper and extending the<br />system to deal with exponentials, we introduce a different formal system describing the intuitionistic character of FILL and we provide a full proof of the cut elimination<br />theorem. The formal system is based on a notion of dependence between formulae within a given proof and seems of independent interest. The procedure for<br />cut elimination applies to (classical) multiplicative Linear Logic, and we can (with care) restrict our attention to the subsystem FILL. The proof, as usual with cut<br />elimination proofs, is a little involved and we have not seen it published anywhere. ER -