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 (7 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  2.  19
    Herbrand complexity and the epsilon calculus with equality.Kenji Miyamoto & Georg Moser - 2023 - Archive for Mathematical Logic 63 (1):89-118.
    The $$\varepsilon $$ -elimination method of Hilbert’s $$\varepsilon $$ -calculus yields the up-to-date most direct algorithm for computing the Herbrand disjunction of an extensional formula. A central advantage is that the upper bound on the Herbrand complexity obtained is independent of the propositional structure of the proof. Prior (modern) work on Hilbert’s $$\varepsilon $$ -calculus focused mainly on the pure calculus, without equality. We clarify that this independence also holds for first-order logic with equality. Further, we provide upper bounds analyses (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  33
    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  
  4.  28
    Herbrand's theorem and term induction.Matthias Baaz & Georg Moser - 2006 - 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 (4 more)  
     
    Export citation  
     
    Bookmark  
  5.  29
    Preface.Arnold Beckmann, Jeremy Avigad & Georg Moser - 2005 - Annals of Pure and Applied Logic 136 (1-2):1-2.
  6.  17
    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  
  8.  15
    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