Epsilon Calculus Provides Shorter Cut-Free Proofs
Matthias Baaz, Anela Lolić · arXiv (Cornell University) · 2024
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.