Proof search tree and cut elimination

Abstract

A new cut elimination method is obtained here by "proof mining" (unwinding) from the following non-effective proof that begins with extracting an infinite branch when the canonical search tree for a given formula E of first order logic is not finite. The branch determines a semivaluation so that and (*) every semivaluation can be extended to a total valuation. Since for every derivation d of E and every model , , this provides a contradiction showing that is finite, . A primitive recursive function L(d) such that is obtained using instead of (*) the statement: For every r, if the canonical search tree with cuts of complexity r∈+∈1 is finite, then is finite. In our proof the reduction of (r∈+∈1)-cuts does not introduce new r-cuts but preserves only one of the branches. © 2008 Springer-Verlag Berlin Heidelberg.