A method of epsilon substitution for the predicate logic with equality

The method of epsilon substitution was defined for arithmetic with interpretation of $\varepsilon xA(x)$ as the least $x$ satisfying $A(x)$. It proceeds by a series of finite approximations “from below” to a solution of a timed system of critical formulas. For the predicate logic only approach “from above” similar to cut-elimination was available. We present a definition of epsilon substitution for the predicate logic, prove the termination of the substitution process, and derive the corresponding Herbrand-type theorem. Bibliography: 18 titles.