Order:
  1. 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 (8 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  2.  12
    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   4 citations  
  3.  10
    Andreas Weiermann. Complexity Bounds for Some Finite Forms of Kruskal's Theorem. Journal of Symbolic Computation, Vol. 18 , Pp. 463–448. - Andreas Weiermann. Termination Proofs for Term Rewriting Systems with Lexicographic Path Ordering Imply Multiply Recursive Derivation Lengths. Theoretical Computer Science, Vol. 139 , Pp. 355–362. - Andreas Weiermann. Bounding Derivation Lengths with Functions From the Slow Growing Hierarchy. Archive of Mathematical Logic, Vol. 37 , Pp. 427–441. [REVIEW]Georg Moser - 2004 - Bulletin of Symbolic Logic 10 (4):588-590.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  4.  19
    Herbrand's Theorem and Term Induction.Matthias Baaz & Georg Moser - 2005 - Archive for Mathematical Logic 45 (4):447-503.
    We study the formal first order system TIND in the standard language of Gentzen's LK . TIND extends LK by the purely logical rule of term-induction, that is a restricted induction principle, deriving numerals instead of arbitrary terms. This rule may be conceived as the logical image of full induction.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  5.  17
    Preface.Arnold Beckmann, Jeremy Avigad & Georg Moser - 2005 - Annals of Pure and Applied Logic 136 (1-2):1-2.
  6.  13
    Journal of Symbolic Computation.Georg Moser - 2004 - Bulletin of Symbolic Logic 10 (4):588-590.
  7. REVIEWS-Three Papers.A. Weiermann & Georg Moser - 2004 - Bulletin of Symbolic Logic 10 (4):588-589.
     
    Export citation  
     
    Bookmark