Lower bounds on Herbrand's theorem

Author:
R. Statman

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

Full-text PDF

Abstract | References | Similar Articles | Additional Information

Abstract: We give non Kalmar-elementary lower bounds on the elimination of quantifier inferences via Herbrand's theorem.

**[1]**Haskell B. Curry and Robert Feys,*Combinatory logic. Vol. I*, With two selections by William Craig. Second printing. Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam, 1968. MR**0244051****[2]**Andrzej Grzegorczyk,*Some classes of recursive functions*, Rozprawy Mat.**4**(1953), 46. MR**0060426****[3]**R. Hindley,*An abstract form of the Church-Rosser theorem. I*, J. Symbolic Logic**34**(1969), 545–560. MR**0302434**, https://doi.org/10.2307/2270849**[4]**-,*An abstract form of the Church-Rosser theorem*. II, J. Symbolic Logic**39**(1974).**[5]**Stephen Cole Kleene,*Introduction to metamathematics*, D. Van Nostrand Co., Inc., New York, N. Y., 1952. MR**0051790****[6]**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****[7]**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.**[8]**-,*Proof-search and speed-up in the predicate calculus*, Ann. Math. Logic (to appear).

Retrieve articles in *Proceedings of the American Mathematical Society*
with MSC:
03F05,
03F20

Retrieve articles in all journals with MSC: 03F05, 03F20

Additional Information

DOI:
https://doi.org/10.1090/S0002-9939-1979-0529224-9

Article copyright:
© Copyright 1979
American Mathematical Society