Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic

Authors Matthias Baaz, Christian G. Fermüller

Thumbnail PDF


  • Filesize: 461 kB
  • 16 pages

Document Identifiers

Author Details

Matthias Baaz
Christian G. Fermüller

Cite AsGet BibTex

Matthias Baaz and Christian G. Fermüller. Elementary Elimination of Prenex Cuts in Disjunction-free Intuitionistic Logic. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 94-109, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


The size of shortest cut-free proofs of first-order formulas in intuitionistic sequent calculus is known to be non-elementary in the worst case in terms of the size of given sequent proofs with cuts of the same formulas. In contrast to that fact, we provide an elementary bound for the size of cut-free proofs for disjunction-free intuitionistic logic for the case where the cut-formulas of the original proof are prenex. Moreover, we establish non-elementary lower bounds for classical disjunction-free proofs with prenex cut-formulas and intuitionistic disjunction-free proofs with non-prenex cut-formulas.
  • Cut-elimination
  • sequent calculus
  • intuitionistic logic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Matthias Baaz and Alexander Leitsch. Cut normal forms and proof complexity. Annals of Pure and Applied Logic, 97(1):127-177, 1999. Google Scholar
  2. Matthias Baaz and Alexander Leitsch. Methods of Cut-elimination. Springer, 2011. Google Scholar
  3. Samuel R. Buss. An introduction to proof theory. In Handbook of Proof Theory, volume 137 of Studies in Logic and the Foundations of Mathematics, pages 1-78. Elsevier, 1998. Google Scholar
  4. Gerhard Gentzen. Untersuchungen über das logische Schließen. I & II. Mathematische Zeitschrift, 39(1):176-210, 405-431, 1935. Google Scholar
  5. Jörg Hudelmaier. Bounds for cut elimination in intuitionistic propositional logic. Archive for Mathematical Logic, 31(5):331-353, 1992. Google Scholar
  6. Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems (TOPLAS), 4(2):258-282, 1982. Google Scholar
  7. V.P. Orevkov. Lower bounds for increasing complexity of derivations after cut elimination. Journal of Soviet Mathematics, 20:2337-2350, 1982. Google Scholar
  8. Richard Statman. Lower bounds on Herbrand’s theorem. Proc. of the Amer. Math. Soc., 75:104-107, 1979. Google Scholar