Lower bounds on Herbrand’s theorem
HTML articles powered by AMS MathViewer
- by R. Statman PDF
- Proc. Amer. Math. Soc. 75 (1979), 104-107 Request permission
Abstract:
We give non Kalmar-elementary lower bounds on the elimination of quantifier inferences via Herbrand’s theorem.References
- Haskell B. Curry and Robert Feys, Combinatory logic. Vol. I, Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam, 1968. With two selections by William Craig; Second printing. MR 0244051
- Andrzej Grzegorczyk, Some classes of recursive functions, Rozprawy Mat. 4 (1953), 46. MR 60426
- R. Hindley, An abstract form of the Church-Rosser theorem. I, J. Symbolic Logic 34 (1969), 545–560. MR 302434, DOI 10.2307/2270849 —, An abstract form of the Church-Rosser theorem. II, J. Symbolic Logic 39 (1974).
- Stephen Cole Kleene, Introduction to metamathematics, D. Van Nostrand Co., Inc., New York, N. Y., 1952. MR 0051790
- G. Kreisel, What have we learnt from Hilbert’s second problem?, Mathematical developments arising from Hilbert problems (Proc. Sympos. Pure Math., Northern Illinois Univ., De Kalb, Ill., 1974) Amer. Math. Soc., Providence, R.I., 1976, pp. 93–130. MR 0434781 R. Statman, Herbrand’s theorem and Gentzen’s notion of a direct proof, in Jon Barwise, ed., Handbook of Mathematical Logic, North-Holland, Amsterdam, 1977, pp. 897-912. —, Proof-search and speed-up in the predicate calculus, Ann. Math. Logic (to appear).
Additional Information
- © Copyright 1979 American Mathematical Society
- Journal: Proc. Amer. Math. Soc. 75 (1979), 104-107
- MSC: Primary 03F05; Secondary 03F20
- DOI: https://doi.org/10.1090/S0002-9939-1979-0529224-9
- MathSciNet review: 529224