Epsilon Calculus Provides Shorter Cut-Free Proofs

Matthias Baaz, Anela Lolic

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 f…