Logical Approaches to Computational Barriers

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 cut-introduction.

websites: Arnold Beckmann | 2008-05-19 |