Formulas for which contraction is admissible
Arnon Avron · Logic Journal of IGPL · 1998
A formula A is said to have the contraction property in a logic L if whenever A, A, Γ ⊨ LB (when Γ is a multiset) also A, Γ & ; LB. 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 (with or without mix) 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 (and others) easily follow. Keywords:substructural logics, linear logic, Gentzen-type systems