# The Epsilon Calculus with Equality and Herbrand Complexity

## TL;DR

This paper analyzes the complexity bounds of Herbrand disjunctions in epsilon calculus with equality, extending previous results and providing new upper and lower bounds for Herbrand's theorem.

## Contribution

It offers the first detailed complexity analysis of Herbrand disjunctions in epsilon calculus with equality, building on and extending prior work without equality.

## Key findings

- Established upper bounds for Herbrand disjunction length with equality.
- Derived lower bounds matching the upper bounds, showing tight complexity estimates.
- Extended the complexity analysis from epsilon calculus without equality to include equality.

## Abstract

Hilbert's epsilon calculus is an extension of elementary or predicate calculus by a term-forming operator $\varepsilon$ 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.