A termination proof for epsilon substitution using partial derivations

Saved in:
Bibliographic Details
Title: A termination proof for epsilon substitution using partial derivations
Authors: Mints, G.1 mints@turing.stanford.edu
Source: Theoretical Computer Science. Jun2003, Vol. 303 Issue 1, p187. 27p.
Subjects: Stochastic convergence, Approximation theory
Abstract: Epsilon substitution method introduced by Hilbert is a successive approximation process providing numerical realizations from proofs of existential formulas. Most convergence (termination) proofs for it use assignments of decreasing ordinals to stages of the process and work only for predicative systems. We describe a new ordinal assignment for the case of first-order arithmetic admitting extension to impredicative systems. It is based on an interpretation of individual epsilon substitutions forming the substitution process as incomplete finite proofs, each encoding a complete but infinite proof. [Copyright &y& Elsevier]
Copyright of Theoretical Computer Science is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
Abstract:Epsilon substitution method introduced by Hilbert is a successive approximation process providing numerical realizations from proofs of existential formulas. Most convergence (termination) proofs for it use assignments of decreasing ordinals to stages of the process and work only for predicative systems. We describe a new ordinal assignment for the case of first-order arithmetic admitting extension to impredicative systems. It is based on an interpretation of individual epsilon substitutions forming the substitution process as incomplete finite proofs, each encoding a complete but infinite proof. [Copyright &y& Elsevier]
ISSN:03043975
DOI:10.1016/S0304-3975(02)00451-6