Herbrand analyses

Archive for Mathematical Logic 30 (5-6):409-441 (1991)
  Copy   BIBTEX


Herbrand's Theorem, in the form of $$\underset{\raise0.3em\hbox{$\smash{\scriptscriptstyle-}$}}{\exists } $$ -inversion lemmata for finitary and infinitary sequent calculi, is the crucial tool for the determination of the provably total function(al)s of a variety of theories. The theories are (second order extensions of) fragments of classical arithmetic; the classes of provably total functions include the elements of the Polynomial Hierarchy, the Grzegorczyk Hierarchy, and the extended Grzegorczyk Hierarchy $\mathfrak{E}^\alpha $ , α < ε0. A subsidiary aim of the paper is to show that the proof theoretic methods used here are distinguished by technical elegance, conceptual clarity, and wide-ranging applicability



    Upload a copy of this work     Papers currently archived: 94,623

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Rekursion über Dilatoren und die Bachmann-Hierarchie.Peter Päppinghaus - 1989 - Archive for Mathematical Logic 28 (1):57-73.


Added to PP

38 (#416,937)

6 months
4 (#1,055,413)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Wilfried Sieg
Carnegie Mellon University

References found in this work

Proof theory.Gaisi Takeuti - 1975 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
On the scheme of induction for bounded arithmetic formulas.A. J. Wilkie & J. B. Paris - 1987 - Annals of Pure and Applied Logic 35 (C):261-302.
Subrecursion: functions and hierarchies.H. E. Rose - 1984 - New York: Oxford University Press.
Fragments of arithmetic.Wilfried Sieg - 1985 - Annals of Pure and Applied Logic 28 (1):33-71.
Grundlagen der Mathematik II.D. Hilbert & P. Bernays - 1974 - Journal of Symbolic Logic 39 (2):357-357.

View all 19 references / Add more references