Linear Logic and Noncommutativity in the Calculus of Structures

[Lutz Strassburger]

Hello,

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 
http://www.loria.fr/~strassbu/
as well as from
http://alessio.guglielmi.name/res/cos/index.html

Best wishes for Christmas and the new year,
Lutz


Title: 
Linear Logic and Noncommutativity in the Calculus of Structures


Abstract:
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.