The Calculus of Structures
Classical 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.

System SKS is a set of rules for classical propositional logic presented in the calculus of structures. Like sequent systems and unlike natural deduction systems, it has an explicit cut rule, which is admissible. In contrast to sequent systems, the cut rule can easily be restricted to atoms. This allows for a very simple cut elimination procedure based on plugging in parts of a proof, like normalisation in natural deduction and unlike cut elimination in the sequent calculus. It should thus be a good common starting point for investigations into both proof search as computation and proof normalisation as computation.

Pdf© Springer-VerlagApril 10, 2003
CSL 2003, LNCS 2803, pp. 86–97 (was Technical Report WV-02-11)BibTeX entry

In this paper we will see deductive systems for classical propositional and predicate logic in the calculus of structures. Like sequent systems, they have a cut rule which is admissible. In addition, they enjoy a top-down symmetry and some normal forms for derivations that are not available in the sequent calculus. Identity axiom, cut, weakening and also contraction can be reduced to atomic form. This leads to rules that are local: they do not require the inspection of expressions of unbounded size.

PdfJanuary 22, 2003
Technical Report WV-03-04, submitted to Archive for Mathematical LogicBibTeX entry

We present an inference system for classical first order logic in which each inference rule, including the cut, only has a finite set of premises to choose from. The main conceptual contribution of this paper is the possibility of separating different sources of infinite choice, which happen to be entangled in the traditional cut rule.

PdfApril 30, 2003
Technical Report WV-03-09, accepted at First Order Logic 75BibTeX entry

The calculus of structures is a framework for specifying logical systems, which is similar to the one-sided sequent calculus but more general. We present a system of inference rules for propositional classical logic in this new framework and prove cut elimination for it. The system also enjoys a decomposition theorem for derivations that is not available in the sequent calculus. The main novelty of our system is that all the rules are local: contraction, in particular, is reduced to atomic form. This should be interesting for distributed proof-search and also for complexity theory, since the computational cost of applying each rule is bounded.

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

I show two simple limitations of sequent systems with multiplicative context treatment: contraction can neither be restricted to atoms nor to the bottom of a proof tree.

PdfAugust 3, 2003
Technical Report WV-02-04, to appear in Logic Journal of the Interest Group in Pure and Applied LogicsBibTeX entry

We show how to get consistency for first order classical logic, in a purely syntactic way, without going through cut elimination. The procedure is very simple and it also shows how finitariness is actually a triviality (contrarily to what one would guess from textbooks).

PdfSeptember 10, 2003It is contained in A Finitary System for First Order Logic
Technical Report WV-02-16BibTeX entry

In this thesis we see deductive systems for classical propositional and predicate logic which use deep inference, i.e. inference rules apply arbitrarily deep inside formulas, and a certain symmetry, which provides an involution on derivations. Like sequent systems, they have a cut rule which is admissible. Unlike sequent systems, they enjoy various new interesting properties. Not only the identity axiom, but also cut, weakening and even contraction are reducible to atomic form. This leads to inference rules that are local, meaning that the effort of applying them is bounded, and finitary, meaning that, given a conclusion, there is only a finite number of premises to choose from. The systems also enjoy new normal forms for derivations and, in the propositional case, a cut elimination procedure that is drastically simpler than the ones for sequent systems.

PdfJuly 15, 2003
PhD thesis, to be defended in 9.2003BibTeX entry

Back to the Calculus of Structures

10.9.2003Alessio Guglielmiemail