2019/04/25 by K. Miyamoto, Kenji Miyamoto, Miyamoto, Kenji +2
Computer Science · Mathematics · #Advanced Combinatorial Mathematics #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Polynomial and algebraic computation #cs.LO #math.LO
paper · pdf · doi:10.48550/arxiv.1904.11304
arxiv created 2019/04/25 · openalex publication_date 2019/04/25 · arxiv updated 2019/07/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Hilbert's epsilon calculus is an extension of elementary or predicate calculus by a term-forming operator ε and initial formulas involving such terms. The fundamental results about the epsilon calculus are so-called epsilon theorems, which have been proven by means of the epsilon elimination method. It is a procedure of transforming a proof in epsilon calculus into a proof in elementary or predicate calculus through getting rid of those initial formulas. One remarkable consequence is a proof of Herbrand's theorem due to Bernays and Hilbert which comes as a corollary of extended first epsilon theorem. The contribution of this paper is the upper and lower bounds analysis of the length of Herbrand disjunctions in extended first epsilon theorem for epsilon calculus with equality. We also show that the complexity analysis for Herbrand's theorem with equality is a straightforward consequence of the one for extended first epsilon theorem without equality due to Moser and Zach.