Exact bounds on epsilon processes (Q535160)

Hilbert introduced the \(\varepsilon\)-substitution method as a potential approach to proving the consistency of Peano arithmetic. The essential idea is to work with finite attempts to find good enough witnesses to all existential statements in a proof. He introduced the H-process, which successively refines such a finite attempt. Consistency of Peano arithmetic then reduces to proving the termination of the H-process. While it is now known how to prove that the H-process for Peano arithmetic, as well as many stronger theories, always terminates, this paper carefully analyzes the number of steps it takes for the process to terminate, in particular characterizing the recursion needed to calculate the length of this process.