Computability in Europe 2006
Logical Approaches to Computational Barriers

Regular Talk:
Proof Fragments and Cut-Elimination

Speaker: Stefan Hetzl
Slot: Array, 11:40-12:00, col. 4


Cut-elimination is a proof transformation of fundamental importance. Originally
it was introduced by Gentzen together with the sequent calculus and it builds
the core of his consistency proof of Peano arithmetic. It also plays an
important role in the analysis of mathematical proofs and has deep connections
to computation in functional programming languages.

Cut-elimination is usually presented as a set of local rewrite rules with some
terminating strategy thus showing the existence of cut-free proofs for all
provable sequents. The changes to the global structure of the proof that are
caused by these local rewrite steps have traditionally been less investigated.

In this talk we consider proof skeletons which are abstract representations of
the structure of proofs. We will describe the changes the skeleton of a proof
undergoes during cut-elimination: Based on its skeleton, a proof with cuts can
be split into several pieces (fragments) which are not broken up further by the
local rewrite rules. The global effect of cut-elimination on the structure of a
proof is therefore shown to be a re-composition of instances of these fragments.

This result allows to describe a certain kind of redundancy whose presence is a
necessary condition for a cut-free proof to allow strong compression by
introduction of cuts. From this characterization follows a lower bound on

websites: Arnold Beckmann 2008-05-19