Switch to: References

Citations of:

Epsilon substitution method for< i> ID_< sub> 1(< i> Π_< sub> 1< sup> 0∨< i> Σ_< sub> 1< sup> 0) [Book Review]

Toshiyasu Arai

Annals of Pure and Applied Logic 121 (2):163-208 (2003)

Add citations

You must login to add citations.

Ideas in the epsilon substitution method for -FIX.Toshiyasu Arai - 2005 - Annals of Pure and Applied Logic 136 (1-2):3-21.details Hilbert proposed the epsilon substitution method as a basis for consistency proofs. Hilbert’s Ansatz for finding a solving substitution for any given finite set of transfinite axioms is, starting with the null substitution S0, to correct false values step by step and thereby generate the process S0,S1,…. The problem is to show that the approximating process terminates. After Gentzen’s innovation, Ackermann [W. Ackermann, Zur Widerspruchsfreiheit der Zahlentheorie, Math. Ann. 117 162–194] succeeded in proving the termination of the process for the (...) Download Export citation Bookmark 6 citations
Epsilon substitution for first- and second-order predicate logic.Grigori Mints - 2013 - Annals of Pure and Applied Logic 164 (6):733-739.details The epsilon substitution method was proposed by D. Hilbert as a tool for consistency proofs. A version for first order predicate logic had been described and proved to terminate in the monograph “Grundlagen der Mathematik”. As far as the author knows, there have been no attempts to extend this approach to the second order case. We discuss possible directions for and obstacles to such extensions. Download Export citation Bookmark 4 citations
The Epsilon Calculus and Herbrand Complexity.Georg Moser & Richard Zach - 2006 - Studia Logica 82 (1):133-155.details Hilbert's ε-calculus is based on an extension of the language of predicate logic by a term-forming operator εx. Two fundamental results about the ε-calculus, the first and second epsilon theorem, play a rôle similar to that which the cut-elimination theorem plays in sequent calculus. In particular, Herbrand's Theorem is a consequence of the epsilon theorems. The paper investigates the epsilon theorems and the complexity of the elimination procedure underlying their proof, as well as the length of Herbrand disjunctions of existential (...) Download Export citation Bookmark 14 citations
2006 Summer Meeting of the Association for Symbolic Logic Logic Colloquium '06: Nijmegen, The Netherlands July 27-August 2, 2006. [REVIEW]Helmut Schwichtenberg - 2007 - Bulletin of Symbolic Logic 13 (2):251-298.details Download Export citation Bookmark
Cut elimination for a simple formulation of epsilon calculus.Grigori Mints - 2008 - Annals of Pure and Applied Logic 152 (1):148-160.details A simple cut elimination proof for arithmetic with the epsilon symbol is used to establish the termination of a modified epsilon substitution process. This opens a possibility of extension to much stronger systems. Download Export citation Bookmark 7 citations
Ackermann’s substitution method.Georg Moser - 2006 - Annals of Pure and Applied Logic 142 (1):1-18.details We aim at a conceptually clear and technically smooth investigation of Ackermann’s substitution method [W. Ackermann, Zur Widerspruchsfreiheit der Zahlentheorie, Math. Ann. 117 162–194]. Our analysis provides a direct classification of the provably recursive functions of , i.e. Peano Arithmetic framed in the ε-calculus. Download Export citation Bookmark 6 citations

1