Removing Syntax from Proof Theory

Alessio Guglielmi

(University of Bath)

In the area of proof complexity we can say much about proofs without worrying about their representation. For example:
On the contrary, in proof theory, we find that proof properties are defined syntactically. A notable example is analyticity, or cut-freeness, and the associated notion of cut elimination.

We could argue that if a notion is syntactic, i.e., only defined in terms of a (possibly elaborate) representation, then it is poorly understood. However, are analyticity and cut elimination eminently syntactic constructions, or is there some underlying natural phenomenon?

In this talk, I argue in favour of the latter, by providing evidence that what we observe in several syntactic settings has a deeper and simpler geometric nature. For example, cut-elimination in propositional logic can be achieved with purely topological means, without any reference to logic. I will also give an idea of a wider effort, based on the newly found geometric methods, aimed at better integrating proof complexity and proof theory, by removing unnecessary syntax.

The talk is based on three recent papers:

A. Guglielmi, T. Gundersen and L. Strassburger. Breaking Paths in Atomic Flows for Classical Logic. LICS 2010. http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf.

A. Guglielmi, T. Gundersen and M. Parigot. A Proof Calculus Which Reduces Syntactic Bureaucracy. RTA 2010. http://drops.dagstuhl.de/opus/volltexte/2010/2649.

P. Bruscoli, A. Guglielmi, T. Gundersen and M. Parigot. A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae. LPAR-16 2010. http://cs.bath.ac.uk/ag/p/QPNDI.pdf.

Journal versions are available at http://alessio.guglielmi.name/res/cos/.
Thursday 9th December 2010, 14:00
Far-134 (Video Conferencing Room)
Department of Computer Science