The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

Isaac Newton Institute for Mathematical Sciences

Semantics of Computation

1 July - 31 December 1995

Organisers: S Abramsky (Imperial College, London), G Kahn (INRIA, Sophia-Antipolis), J C Mitchell (Stanford), A M Pitts (Cambridge)

Semantics of Computation Seminar

Monday 11 December, 2pm

Some combinatorics behind proofs

A.Carbone (Technical University of Vienna)

We try to bring to light some combinatorial structure underlying formal proofs in logic. We do this through the study of the Craig Interpolation Theorem which is properly a statement about the structure of formal derivations. We show that there is a generalization of the interpolation theorem to much more naive structures about sets, and then we show how both classical and intuitionistic versions of the statement follow by interpreting properly the set-theoretic language.

The theorem we present is a geometrical formulation of the well-known logical statement and gives sufficient conditions for a system of combinatorial nature to enjoy interpolation. Its objects might be graphs just as well as formulas or surfaces.

The combinatorial mappings we use correspond whenever interpreted in a logical language to the notion of `logical flow graph' (i.e. a graph tracing the flow of occurrences of formulas in a proof; this notion has been introduced in [Buss, 1991]. The idea of using the flow of occurrences to study the structure of proofs was already present in [Girard, 1987] with the concept of `proof net'.)

This analysis was partly motivated by the close relation that exists between complexity bounds of interpolants and the problem of knowing whether NP intersect CO-NP is contained in P/poly.

Copyright © Isaac Newton Institute