Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Epsilon Calculus Provides Shorter Cut-Free Proofs

Matthias Baaz, Anela Lolic

Abstract

In this paper we show that cut-free derivations in the epsilon format of sequent calculus provide for a non-elementary speed-up w.r.t. cut-free proofs in usual sequent calculi in first-order language.

Epsilon Calculus Provides Shorter Cut-Free Proofs

Abstract

In this paper we show that cut-free derivations in the epsilon format of sequent calculus provide for a non-elementary speed-up w.r.t. cut-free proofs in usual sequent calculi in first-order language.
Paper Structure (5 sections, 8 theorems, 5 equations)

This paper contains 5 sections, 8 theorems, 5 equations.

Table of Contents

  1. Introduction
  2. Epsilon Calculus
  3. ${\bf L}\varepsilon$, ${\bf LK}$, and Related Sequent Calculi
  4. ${\bf LK}^{+}$ and ${\bf LK}^{++}$
  5. Conclusion

Key Result

proposition 1

Every ${\bf LK}$-derivation possibly with cuts can be translated into an ${\bf L}\varepsilon$-derivation of equal or smaller length.

Theorems & Definitions (24)

  • definition 1: ${\bf L}\varepsilon$
  • definition 2
  • proposition 1
  • proof
  • remark 1
  • theorem 1: orevkov1982lowerstatman1979lower
  • corollary 1
  • proof
  • definition 3
  • lemma 1
  • ...and 14 more