A method of epsilon substitution for the predicate logic with equality (Q1807464)

The method of epsilon substitution for arithmetic proposed by Hilbert proceeds by a series of finite approximations ``from below'' to a solution of a fixed system of critical formulas. Ackermann applied the method also to the first order predicate logic with equality and extensionality formalized in terms of the epsilon symbol, which however proceeds ``from above'' by replacing the epsilon-terms of highest complexity similarly to cut-elimination. In this paper, the author provides for the predicate logic and its extensions by equality and extensionality, respectively, a method of epsilon substitution ``from below'' resembling Hilbert's original program, and proves the strong termination of the substitution process which corresponds to the strong normalizability in cut-elimination and is not obtained by Ackermann's method. As an application, a Herbrand-type theorem is shown to hold for the respective epsilon calculus.