Alessandra Carbone

Technical University of Vienna

Interpolants and Dynamics of Cut-elimination

DIMACS Center - Room 431

Busch Campus

Piscataway, New Jersey

April 26, ** 1:30 ** p.m.

Abstract:

We consider the Craig Interpolation Theorem for the propositional sequent calculus _with_ cuts (which is polynomially equivalent to Frege Systems) and we look at tautologies A(p_1,..., p_n) -> B(q_1, ... , q_k) where A and B do not have variables in common. We know that either A-> or ->B is a provable sequent and we ask whether there is a proof of A-> or a proof of ->B which is polynomially bounded in the original proof of A->B.

For cut-free proofs the answer is positive but for proofs with cuts the question is open. The difficulties seem to lie in the dynamics of the procedure of cut-elimination. The talk will be dedicated to the analysis of the dynamical properties of the unwinding of a proof with cuts into a proof without cuts.

The results we will present are based on an analysis of graphs associated to proofs (i.e. a finite graph which traces the flow of occurrences of formulas in proofs; this notion has been introduced in [Buss, 1991]. The idea of using the flow of occurrences to study the structure of proofs was present in [Girard, 1987] with the concept of `proof net'.)