Strong termination for the epsilon substitution method
Grigori Mint︠s︡ · Journal of Symbolic Logic · 1996
Abstract Ackermann proved termination for a special order of reductions in Hilbert's epsilon substitution method for the first order arithmetic. We establish termination for arbitrary order of reductions.