Switch to: References

Add citations

You must login to add citations.
  1. Ideas in the epsilon substitution method for -FIX.Toshiyasu Arai - 2005 - Annals of Pure and Applied Logic 136 (1-2):3-21.
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • Epsilon substitution for transfinite induction.Henry Towsner - 2005 - Archive for Mathematical Logic 44 (4):397-412.
    We apply Mints’ technique for proving the termination of the epsilon substitution method via cut-elimination to the system of Peano Arithmetic with Transfinite Induction given by Arai.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • Epsilon substitution for $$\textit{ID}_1$$ ID 1 via cut-elimination.Henry Towsner - 2018 - Archive for Mathematical Logic 57 (5-6):497-531.
    The \-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory \ using a variant of the cut-elimination formalism introduced by Mints.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Epsilon Substitution Method for [image] -FIX.Toshiyasu Arai - 2006 - Journal of Symbolic Logic 71 (4):1155 - 1188.
    In this paper we formulate epsilon substitution method for a theory $\Pi _{2}^{0}$-FIX for non-monotonic $\Pi _{2}^{0}$ inductive definitions. Then we give a termination proof of the H-processes based on Ackermann [1].
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • Ackermann’s substitution method.Georg Moser - 2006 - Annals of Pure and Applied Logic 142 (1):1-18.
    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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • Cut elimination for a simple formulation of epsilon calculus.Grigori Mints - 2008 - Annals of Pure and Applied Logic 152 (1):148-160.
    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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  • Epsilon substitution method for [Π0 1, Π0 1]-FIX.T. Arai - 2005 - Archive for Mathematical Logic 44 (8):1009-1043.
    We formulate epsilon substitution method for a theory [Π0 1, Π0 1]-FIX for two steps non-monotonic Π0 1 inductive definitions. Then we give a termination proof of the H-processes based on Ackermann [1].
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • Epsilon substitution method for< i> ID< sub> 1(< i> Π_< sub> 1< sup> 0∨< i> Σ< sub> 1< sup> 0). [REVIEW]Toshiyasu Arai - 2003 - Annals of Pure and Applied Logic 121 (2):163-208.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • Epsilon substitution method for ID1.Toshiyasu Arai - 2003 - Annals of Pure and Applied Logic 121 (2-3):163-208.
    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 162) succeeded to prove termination of the process for first order arithmetic. Inspired by G. Mints as an Ariadne's (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   20 citations  
  • Exact bounds on epsilon processes.Toshiyasu Arai - 2011 - Archive for Mathematical Logic 50 (3-4):445-458.
    In this paper we show that the lengths of the approximating processes in epsilon substitution method are calculable by ordinal recursions in an optimal way.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation