 The version of Herbrand’s theorem stated at the beginning of this section is essentially the special case of (2) in which the formula \(A\) is existential. In light of this special case, (1) is equivalent to the assertion that a formula \(A\) is derivable in first-order predicate logic if and only if \(A^H\) is. The forward direction of this equivalence is much easier to prove; in fact, for any formula \(A, A \rightarrow A^H\) is derivable in predicate logic. Proving the reverse direction involves eliminating the additional function symbols in \(A^H\), and is much more difficult, especially in the presence of equality. It is here that epsilon methods play a central role.