 Hilbert and Bernays used the methods of the epsilon calculus to establish theorems about first order logic that make no reference to the epsilon calculus itself. One such example is Herbrand’s theorem (Herbrand 1930; see Buss 1995, Girard 1982, and section 2.5 of Buss 1998). This is often formulated as the statement that if  an existential formula \[ \exists x_1 \ldots \exists x_k A(x_1, \ldots, x_k) \] is derivable in first-order predicate logic (without   equality), where \(A\) is quantifier-free, then there are sequences of terms \(t_{1}^1, \ldots, t_{k}^1, \ldots, t_{1}^n, \ldots, t_k ^n\),   such that \[ A(t_{1}^1, \ldots, t_k ^1) \vee \ldots \vee A(t_{1}^n, \ldots, t_k^n) \] is a tautology. If one is dealing with first-order   logic with equality, one has to replace “tautology” by “tautological consequence of substitution instances of the equality axioms”; we will use the term “quasi-tautology” to describe such a formula.