- The notion of proof system is remarkably non-syntactic: a proof system is any algorithm that checks proofs in polynomial time.
- The class of Frege propositional systems is robust: they all are polynomially equivalent, independently of the base of connectives and the choice of inference rules.

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/.

Far-134 (Video Conferencing Room)

Department of Computer Science