Affordable Access

Publisher Website

A termination proof for epsilon substitution using partial derivations

Authors
Journal
Theoretical Computer Science
0304-3975
Publisher
Elsevier
Publication Date
Volume
303
Issue
1
Identifiers
DOI: 10.1016/s0304-3975(02)00451-6
Keywords
  • Epsilon Substitution Method
  • Infinite Proofs
  • Incomplete Proofs
  • Extraction Of Programs
Disciplines
  • Mathematics

Abstract

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.

There are no comments yet on this publication. Be the first to share your thoughts.