Abstract

A formula A is said to have the contraction property in a logic L if whenever A, A, Γ ⊨ L B also A, Γ & ; L B. In MLL and in MALL without the additive constants a formula has the contraction property if it is a theorem. Adding the mix rule does not change this fact. In MALL and in affine logic A has the contraction property if either A is provable of A is equivalent to the additive constant 0. We present some general proof-theoretical principles from which all these results easily follow