Lógica, Provas e Algoritmos

Alessandra Carbone

Cut Elimination and the Structure of Proofs (Tutorial)

We give an introduction to the study of proof structure for proofs with modus ponens. More precisely we work in the sequent calculus LK (Gentzen, 1932) and we study the properties of the logical flow graphs (Buss, 1991) of proofs in this system.
We survey classical results due to Statman, Tseitin, Orevkov, Haken and others on the complexity of proofs with and without cuts.
Our main concern will be to analyse proofs during the process of cut-elimination through which we will try to bring to light the strong geometric and dynamical flavor lying inside proofs.
The interest in this study relies on the links with classical problems in complexity theory as well as algorithmic aspects of proofs. The talk will focus on both views.

Combinatorics Explains the Structure of Proofs and the Complexity of Cut Elimination

We introduce a purely combinatorial model which explains structural properties of proofs as well as the complexity of cut-elimination. Proofs are two-dimensional objects and differences in the behavior of their cut-elimination can often be accounted for by differences in their two-dimensional structure. Based on these latter, we will give upper and lower bounds for cut-elimination.
We will present here ground material.
Part of the work presented in this talk has been done in collaboration with Stephen Semmes.

Short Proofs Must Contain Cycles - ALK: An Acyclic Proof System

"Short" proofs in predicate logic contain cycles in their logical flow graph. We give a proof of this statement and present a new proof system which is close to Linear Logic in spirit, enjoys cut-elimination, it is acyclic and its proofs are only elementary larger than proofs in LK. The proofs in the new calculus can be obtained by a small perturbation of proofs in LK and they represent a geometrical alternative for studying structural properties of LK-proofs. They satisfy the constructive disjunction property and most important, simpler geometrical properties of their logical flow graphs. The geometrical counterpart to a cycle in LK is represented in the new setting by a spiral.

Cut-Free Proofs are `Easy': The Craig Interpolation Theorem Holds for More Complicated Geometric Structures

The Craig Interpolation Theorem is a statement about the structure of formal derivations. It says that given two logical formulas A and B such that A implies B is provable, there is a formula I called an interpolant for A and B such that I can be expressed in the language common to A and B and such that A implies I and I implies B are provable.
One way to prove this result is to transform a proof of A implies B into its cut-free form and build out of this latter proof an interpolant I as well as proofs for A implies I and I implies B.
We generalize this theorem to much more naïve structures about sets and show how interpolation can be seen as a general combinatorial phenomenon which does not depend on the specific choice of structure for the underlying sets. Our statement holds for graphs, as well as formulas or surfaces.
We will comment on the meaning of this result on the light of fundamental questions of complexity theory which concern the complexity of interpolants and the problem of knowing whether NP \cup co-NP is contained in P/poly.