Ackermann’s substitution method (remixed)

We aim at a conceptually clear and technically smooth investigation of Ackermann’s substitution method [W. Ackermann, Zur Widerspruchsfreiheit der Zahlentheorie, Math. Ann. 117 (1940) 162–194]. Our analysis provides a direct classification of the provably recursive functions of , i.e. Peano Arithmetic framed in the ε-calculus.