Lógica, Provas e Algoritmos
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
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