Switch to: References

Add citations

You must login to add citations.
  1. 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 (6 more)  
     
    Export citation  
     
    Bookmark  
  • The Epsilon Calculus and Herbrand Complexity.Georg Moser & Richard Zach - 2006 - Studia Logica 82 (1):133-155.
    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 (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  • The Epsilon Calculus.Jeremy Avigad & Richard Zach - 2008 - In Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy. The Metaphysics Research Lab, Center for the Study of Language and Information, Stanford University.
    The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term εx A denotes some x satisfying A(x), if there is one. In Hilbert's Program, the epsilon terms play the role of ideal elements; the aim of Hilbert's finitistic consistency proofs is to give a procedure which removes such terms (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  • 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