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.
- Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
- Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX
- Epsilon substitution for first- and second-order predicate logic
- A termination proof for epsilon substitution using partial derivations
- Epsilon substitution method for theories of jump hierarchies
- Epsilon substitution method for -FIX
- Epsilon substitution method for \([\Pi^0_1,\Pi^0_1]\)-FIX
- Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
- Epsilon substitution method for theories of jump hierarchies
- Functionals defined by transfinite recursion
- Ideas in the epsilon substitution method for \(\Pi_{1}^{0}\)-FIX
- Nested recursion
This page was built for publication: Exact bounds on epsilon processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q535160)
