Linear Logic and Noncommutativity in the Calculus of Structures

Lutz Strassburger Lutz.Strassburger at
Thu Dec 18 18:02:52 EST 2003


I would like to announce my PhD-thesis (defended on 24 July 2003) which might 
be interesting for people in the types and proof theory lists. Feedback is 
very welcome. The pdf-file is available from
as well as from

Best wishes for Christmas and the new year,

Linear Logic and Noncommutativity in the Calculus of Structures

In this thesis I study several deductive systems for linear logic, 
its fragments, and some noncommutative extensions.  All systems will 
be designed within the calculus of structures, which is a proof
theoretical formalism for specifying logical systems, in the tradition
of Hilbert's formalism, natural deduction, and the sequent calculus.
Systems in the calculus of structures are based on two simple
principles: deep inference and top-down symmetry.  Together they have
remarkable consequences for the properties of the logical systems. For
example, for linear logic it is possible to design a deductive system,
in which all rules are local.  In particular, the contraction rule is
reduced to an atomic version, and there is no global promotion rule. 
I will also show an extension of multiplicative exponential linear 
logic by a noncommutative, self-dual connective which is not
representable in the sequent calculus.  All systems enjoy the cut 
elimination property.  Moreover, this can be proved independently
from the sequent calculus via techniques that are based on the new 
top-down symmetry.  Furthermore, for all systems, I will present 
several decomposition theorems which constitute a new type of normal 
form for derivations.

More information about the Types-list mailing list