Elementary cut-elimination for prenex cuts in disjunction free LJ
Abstract:
The elimination of cuts (lemmas) from given sequent calculus proofs has remained in the focus of proof theory ever since Gentzen's seminal paper from 1934/35. It is well known that the worst case complexity of cut-elimination is non-elementary for first-order intuitionistic as well as classical logic. No elementary upper bound for cut-elimination seems to be known for non-trivial genuine first-order fragments of intuitionistic logics. The purpose of this paper is to show that one can in fact eliminate cuts involving only prenex cut-formulas from disjunction-free intuitionistic sequent proofs without non-elementary increase in the size of proofs. The result is sharp in several respects. As we will show, in all of the following cases there exist non-elementary lower bounds for cut-elimination:
(1) classical disjunction-free proofs with quantified atomic cuts
(2) intuitionistic disjunction-free proofs with infix cuts,
(3) intuitionistic proofs with prenex cuts in the presence of disjunction.
(joint work with Chris Fermüller, Vienna University of Technology)
EN
