Epsilon Calculus Provides Shorter Cut-Free Proofs

2024/01/17 by Matthias Baaz, Baaz, Matthias, Anela Lolić +1
Computer Science · #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics, Computing, and Information Processing

paper · pdf · doi:10.48550/arxiv.2401.09183

openalex publication_date 2024/01/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• A theory of cut-restriction: first steps
• Cut-restriction: from cuts to analytic cuts
• Lectures on the Epsilon Calculus
• The Cut Elimination and the Nonlengthening Property for the Sequent Calculus with Equality
• The Epsilon Calculus with Equality and Herbrand Complexity