The Calculus of Structures

Electric lamps were not invented by improving candles

Contents of this page

1. Frequently Asked Questions
2. Papers, Lectures and Theses
   1. Classical Logic
   2. Linear Logic
   3. Modal Logics
   4. Commutative/Non-commutative Linear Logic
   5. Cyclic Linear Logic
   6. Language Design
3. Notes, Conjectures, Problems, Etc.
4. Proof Theory Mailing List
5. Politics
6. Acknowledgements

Related links

• Group at TU Dresden (people, events, funding and resources)
• ProofTheory.ORG
• Summer School and Workshop on Proof Theory, Computation and Complexity (Dresden 2003)
• Workshop on Proof Theory and Computation (Dresden 2002)

The calculus of structures is a new proof theoretical formalism, introduced by myself in 1999 and mostly developed by members of our group in Dresden since 2000. It exploits a new top-down symmetry of derivations made possible by deep inference. We can present deductive systems in the calculus of structures and analyse their properties, as we do in the sequent calculus, natural deduction and proof nets. Typical properties of interest are normalisation and cut elimination.

The main purpose of our new formalism is to allow a richer combinatorial analysis of proofs than the other formalisms do. We adopted two main ideas: inferences are symmetric between premises and conclusions, and they are deeply applicable inside expressions (what we call `deep inference´). As a consequence, it is convenient to deduce over structures, which are expressions intermediate between formulae and sequents.

The proof theory of the calculus of structures differs significantly from what has been studied so far. Deep inference severely challenges the usual cut elimination methods, but this is mitigated by atomic cuts being much simpler objects than generic cuts.

We developed several new techniques to overcome the difficulties. Some of these methods allowed us to unveil totally new combinatorial properties of logical systems, like the decomposition theorems. In general, the new properties have a strong flavour of modularity. This, together with atomicity and locality, is important for applications in computer science, which we recently started to pursue.

So far, we presented classical logic and linear logic (in all its fragments) in the calculus of structures, in such a way that atomicity, locality and the various instances of modularity have been expressed. We are currently studying several modal logics, with equally pleasing results. In collaboration with external researchers, we are investigating intuitionistic logics and non-commutative linear logics, like Yetter's cyclic linear logic and Abrusci-Ruet non-commutative logic. The deductive systems in the calculus of structures are simple and elegant, and they pose no special challenge to those interested in using them.

This whole theory was born when trying to capture a hybrid commutative/non-commutative logic, which I call system V. Only the multiplicative fragment of V has been developed so far—again with all the good properties mentioned above. Despite its simplicity (only three inference rules), this system cannot be presented in the sequent calculus. This is rather surprising and allows us to claim our ability to extend the range of application of the sequent calculus, the most versatile formalism so far.

1. General
   1. Isn't the calculus of structures just a trivial notational variation of the sequent calculus?
   2. Proof theory is famous for producing horrible proofs of its own theorems; are you doing any better?
   3. What is deep inference?
   4. What is a structure?
   5. Isn't the word `structure´ reserved for semantics?
   6. Can you do in the calculus of structures anything you can do in the sequent calculus?
   7. Does the calculus of structures automatically introduce a mix rule in any system?
2. Cut Elimination
   1. You make a big deal of having the cut rule in atomic form; but can't you do the same in the sequent calculus?
   2. What's the point in proving again cut elimination for classical and linear logic?
   3. By the way, what's the point in dedicating an entire paper to such an easy statement as cut elimination for propositional classical logic in the calculus of structures?
3. Term Rewriting
   1. Isn't a system in the calculus of structures just a term rewriting system (modulo an equational theory)?
   2. If so, why not using the term rewriting terminology and conventions?
   3. But then what about rewriting logic?
4. Philosophy
   1. Do the inference rules in the calculus of structures have an associated theory of meaning, like the inference rules in the sequent calculus and natural deduction?

Full FAQ page

The following material is broad in scope:

Mismatch
Alessio Guglielmi
PdfAugust 24, 2003
Brief note for the specialist, recently posted to the Foundations of Mathematics and Proof Theory lists. It introduces the calculus of structures by addressing the problem of a mismatch between object and meta level.

Deep Inference and Symmetry in Classical Proofs
Kai Brünnler
PdfJuly 15, 2003
PhD thesis, to be defended on 22.9.2003BibTeX entry

Linear Logic and Noncommutativity in the Calculus of Structures
Lutz Straßburger
PdfPdf in booklet formatJuly 25, 2003
PhD thesis, successfully defended on 24.7.2003BibTeX entry

Proof Theory With Deep Inference—Slide Presentation
Alessio Guglielmi
PdfJune 28, 2003
Course at Summer School and Workshop on Proof Theory, Computation and Complexity

Deep Inference—Slide Presentation
Alessio Guglielmi
PdfMarch 13, 2003
Talk

The Calculus of Structures—Project Report
Alessio Guglielmi
PdfSeptember 10, 2003
Always outdated but sometimes updated; this report assumes you are familiar with structural proof theory; it gives an overview of the activity in our group

Papers are divided into six sections according to their subject: classical logic, modal logics, linear Logic, commutative/non-commutative linear logic, cyclic linear logic and language design. Each paper presents an introduction to the calculus of structures. There is no general introduction to the calculus yet, because we started developing it from concrete examples, i.e., deductive systems. Inside each section, papers are listed in decreasing order of accessibility.

It is important to bear in mind a terminological distinction we make: a (formal) system is a set of inference rule schemes, a calculus is the formalism in which the formal systems are designed. For example, system LK is a formal system for classical logic in the sequent calculus.

2.1Classical Logic

So far, for classical logic in the calculus of structures it has been achieved:

• the cut rule trivially reduces to atomic form;
• one can show cut elimination for the propositional fragment by the simplest argument to date;
• the propositional fragment is fully local, including contraction;
• first order classical logic can be entirely made finitary;
• cut elimination and decomposition theorems are proved.

Atomic Cut Elimination for Classical Logic
Kai Brünnler
Pdf© Springer-VerlagApril 10, 2003
CSL 2003, LNCS 2803, pp. 86–97 (was Technical Report WV-02-11)BibTeX entry

Locality for Classical Logic
Kai Brünnler
PdfJanuary 22, 2003
Technical Report WV-03-04, submitted to Archive for Mathematical LogicBibTeX entry

A Finitary System for First Order Logic
Kai Brünnler and Alessio Guglielmi
PdfApril 30, 2003
Technical Report WV-03-09, accepted at First Order Logic 75BibTeX entry

A Local System for Classical Logic
Kai Brünnler and Alwen Fernanto Tiu
Pdf© Springer-VerlagOctober 2, 2001It was Technical Report WV-01-02, now replaced by Locality for Classical Logic
LPAR 2001, LNAI 2250, pp. 347–361BibTeX entry

Two Restrictions on Contraction
Kai Brünnler
PdfAugust 3, 2003
Technical Report WV-02-04, to appear in Logic Journal of the Interest Group in Pure and Applied LogicsBibTeX entry

Consistency Without Cut Elimination
Kai Brünnler and Alessio Guglielmi
PdfSeptember 10, 2003It is contained in A Finitary System for First Order Logic
Technical Report WV-02-16BibTeX entry

Classical logic in the calculus of structures (abstracts)

2.2Linear Logic

So far, for linear logic in the calculus of structures it has been achieved:

• the cut rule trivially reduces to atomic form;
• the propositional fragment is fully local, including promotion and contraction;
• cut elimination and decomposition theorems are proved.

A Local System for Linear Logic
Lutz Straßburger

• Conference version pdf© Springer-VerlagAugust 9, 2002
  LPAR 2002, LNAI 2514, pp. 388–402BibTeX entry
• Work-in-progress technical report pdfJune 10, 2002
  Technical Report WV-02-01BibTeX entry

MELL in the Calculus of Structures
Lutz Straßburger
PdfOctober 29, 2001This paper is contained in succinct form in Non-commutativity and MELL in the Calculus of Structures
Technical Report WV-01-03, to appear in Theoretical Computer ScienceBibTeX entry

Linear logic in the calculus of structures (abstracts)

2.3Modal Logics

Several normal propositional modal logics are systematically presented in the calculus of structures and cut elimination is proved.

A Systematic Proof Theory for Several Modal Logics
Charles Stewart and Phiniki Stouppa
PdfApril 16, 2003
Technical Report WV-03-08BibTeX entry

Modal logics in the calculus of structures (abstract)

2.4Commutative/Non-commutative Linear Logic

We conservatively extend mixed multiplicative and multiplicative exponential linear logic with a self-dual non-commutative operator. The systems so obtained cannot be presented in the sequent calculus, but they enjoy the usual properties of locality, decomposition and cut elimination available in the calculus of structures.

Non-commutativity and MELL in the Calculus of Structures
Alessio Guglielmi and Lutz Straßburger
Pdf© Springer-VerlagJune 28, 2001
CSL 2001, LNCS 2142, pp. 54–68 (was Technical Report WV-01-04)BibTeX entry

A System of Interaction and Structure
Alessio Guglielmi
PdfSeptember 27, 2002
Technical Report WV-02-10, submitted to ACM Transactions on Computational LogicBibTeX entry

Properties of a Logical System in the Calculus of Structures
Alwen Fernanto Tiu
PdfSeptember 12, 2001
MSc thesis, successfully defended on 1.8.2001, Technical Report WV-01-06BibTeX entry

A Non-commutative Extension of Multiplicative Exponential Linear Logic
Alessio Guglielmi and Lutz Straßburger

• Conference version pdf© Springer-VerlagAugust 9, 2002
  LPAR 2002, LNCS 2514, pp. 231–246BibTeX entry
• Journal version pdfJuly 4, 2003
  Technical Report WV-02-03, submitted to APALBibTeX entry

The Undecidability of System NEL
Lutz Straßburger

• Conference version pdfAugust 20, 2003
  accepted at WoLLIC 2003 under the title System NEL Is Undecidable, to appear in ENTCSBibTeX entry
• Journal version pdfFebruary 12, 2003
  Technical Report WV-03-05BibTeX entry

A1-Unification
Alwen Fernanto Tiu
Gzipped PostscriptFebruary 19, 2002
Technical Report WV-01-08BibTeX entry

Combining A1- and AC1-Unification Sharing Unit
Alwen Fernanto Tiu
Gzipped PostscriptFebruary 19, 2002
Technical Report WV-01-09BibTeX entry

Commutative/non-commutative linear logic in the calculus of structures (abstracts)

2.5Cyclic Linear Logic

Yetter's cyclic linear logic is presented in the calculus of structures and cut elimination is proved. Interestingly, cyclicity is naturally subsumed by deep inference.

Structures in Cyclic Linear Logic
Pietro Di Gianantonio
Gzipped PostscriptFebruary 12, 2003
Technical Report, Università di UdineBibTeX entry

Cyclic linear logic in the calculus of structures (abstract)

2.6Language Design

Thanks to a self-dual non-commutative extension of linear logic one gets the first purely logical account of sequentiality in proof search.

A Purely Logical Account of Sequentiality in Proof Search
Paola Bruscoli
Pdf© Springer-VerlagAugust 12, 2002
ICLP 2002, LNCS 2401, pp. 302–316 (was Technical Report WV-02-06)BibTeX entry

Language design in the calculus of structures (abstract)

Freedom from BureaucracyF.F.The dream of flying above the miseries of syntax can be realised provided all ties with totalitarian ideologies are cut.February 15, 1963

Goodness, Perfection and MiraclesA.G.I introduce three properties closely related to cut elimination and interpolation theorems. October 18, 2002

RecipeA.G.A family of tautologies that hold in most logics can be used, following a simple recipe, to produce deductive systems where all rules are local, including cut.October 27, 2002

Finitary CutA.G.We all know that the traditional cut rule is considered infinitary. But if we reduce the cut rule to atomic form, as we always can do in the calculus of structures, is atomic cut still infinitary? Not really.October 23, 2002This note is now subsumed by A Finitary System for First Order Logic

On Lafont's CounterexampleA.G.Lafont's counterexample shows why cut elimination in the sequent calculus of classical logic is not confluent. I show here that the counterexample doesn't work in the calculus of structures.November 1, 2002

Normalisation Without Cut EliminationA.G.I propose a possible notion of equivalence for proofs in classical logic, sort of a normal form for case analysis.February 25, 2003

ButterfliesA.G.It's not known whether MELL is decidable. I conjecture here that system NEL, i.e., MELL plus non-commutativity, is undecidable. I propose an encoding of Post's Correspondence Problem (PCP) into NEL that has the merit of making non–commutativity (in NEL) correspond to sequential composition (in PCP), which is intuitive.November 1, 2002

Subatomic LogicA.G.One can unify classical and linear logic by using only two simple, linear, `hyper´ inference rules; they generate nice systems for all the fragments, where all rules are local. The various logics are determined by the algebra of their units, for example boolean algebra determines classical logic. We can prove cut elimination easily and once and for all in the two-rule system, and the procedure scales down to all the derived fragments.November 21, 2002

Minimal Logic in the Calculus of StructuresK.B.In this note I present preliminary ideas about a system for minimal logic.February 12, 2003

I help running a mailing list devoted to proof theory, where the calculus of structures is sometimes discussed: click here to subscribe or here to unsubscribe.

More on the list

Since a few years I'm criticizing the current practice of publishing papers at conferences, in theoretical computer science. I decided not to send papers to, or participate in conferences, in any way, including reviewing. Of course this is an extremist position (and perhaps an irrelevant one), but I feel that everybody in life should choose a little radical campaign to fight. In order not to endanger too much the career of my colleagues, I accepted to co-author some conference papers with them.

The reasons for my choice are the following. There are too many conferences and it is too easy to publish papers. Since conference publication has some weight in assessing CVs, it is highly encouraged, and thanks to it people are able to put together massive CVs to slam on the face of their adversaries. Given the inflation of papers, the attention devoted to reviewing them is forcefully limited. Moreover, conference papers are usually written under time pressure and format constraints, which do not facilitate the task of communicating.

Conferences, like mobile phones and cars, are locally good but globally bad. While it might be nice and fruitful to participate in a conference occasionally, a system where an entire community is forced to jump from plane to plane, sleeplessly trying to write and review tons of paper, is dangerous to the healthy development of theoretical computer science. Breakthrough ideas require constant effort and continuous attention, they do not come out of brownian motion.

The development of the calculus of structures took me several years, the first five of which spent in recycling paper. I started at University of Pennsylvania (1994), then went on at Università di Pisa (1994-97) and INRIA Lorraine (1997-98), and then at TU Dresden.

The following persons profoundly influenced the building of the calculus of structures:

• Jean-Yves Girard: I took from him the conviction that there are deep geometrical phenomena at the basis of proof theory, and I found inspiration in linear logic.
• Giorgio Levi and Dale Miller: Giorgio made me read and work on Dale's papers, where I could find excellent design of logical systems.
• Christian Retoré: he made me interested in the strange properties of self-duality and non-commutativity and their challenge to proof theory, and he also pointed me to N-free orders, which is where everything started finally to work and make sense.

At TU Dresden I found three crazy, extraordinary students: Kai Brünnler, Lutz Straßburger and Alwen Tiu. They risked their future careers to come working on this project at a time when nobody sane could bet on its success.

Last, but not least, I'd like to acknowledge the excellent education I've got at the Scuola Normale Superiore, at a time when I didn't know that proof theory existed, nor did I know the value of education.

10.9.2003Alessio Guglielmiemail