Investigating Bounded Contraction
Andreja Prijatelj

Abstract:
The thesis is a collection of four self-contained papers investigating
meta-properties of intuitionistic and classical Gentzen systems with bounded
contraction and their algebraic models.

Two versions of bouded contraction are considered, differing in the restriction
imposed on the usual contraction rule:
  s-contraction, where contraction is restricted to a certain basic type
    (or equivalently, atomic formula);
  n-contraction, for n greater or equal 2, where (n+1)occurrences of a
    formula may be contracted to n occurrences.
Substituting s-contraction or n-contraction for full contraction in Gentzen
systems already results in splitting of connectives familiar from linear logic.

Thus particular fragments of intuitionistic and classical linear logic extended with bounded contraction and their affine extensions are explored throughout 
this work. There is, however a crucial distinction between the two versions of 
contraction from the proof theoretical point of view. Linear systems with 
s-contraction retain the cut-elimination property as opposed to those with
n-contraction.

As a result this work can naturally be divided into:
  proof theoretical part I, and
  algebraic parts II, III, and IV.

The papers collected in this thesis are the following:
   (I) Lambek Calculus with Restricted Contraction and Expansion, 1992,
       Studia Logica 51, 125-143.
  (II) Bounded Contraction and Gentzen-style Formulation of Lukasiewicz Logics,
       to appear in Studia Logica.
 (III) Connectification for n-Contraction, to appear in Studia Logica.
  (IV) Free Algebras Corresponding to Multiplicative Classical Linear Logic and
       some Extensions, 1994, ILLC Prep. Series, ML-94-08,
       University of Amsterdam.