Remote Access Proceedings of the American Mathematical Society
Green Open Access

Proceedings of the American Mathematical Society

ISSN 1088-6826(online) ISSN 0002-9939(print)

 
 

 

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 Free Access

Abstract | References | Similar Articles | Additional Information

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


References [Enhancements On Off] (What's this?)

  • [1] H. B. Curry and R. Feys, Combinatory logic, Vol. 1, North-Holland, Amsterdam, 1968. MR 0244051 (39:5368)
  • [2] A. Grzegorczyk, Some classes of recursive functions, Rozprawy Mat. 4 (1953). MR 0060426 (15:667d)
  • [3] R. Hindley, An abstract form of the Church-Rosser theorem. I, J. Symbolic Logic 34 (1969). MR 0302434 (46:1578)
  • [4] -, An abstract form of the Church-Rosser theorem. II, J. Symbolic Logic 39 (1974).
  • [5] S. C. Kleene, Introduction to metamathematics, Van Nostrand, Princeton, N.J., 1952. MR 0051790 (14:525m)
  • [6] G. Kreisel, What have we learnt from Hilbert's second problem, in Proc. Sympos. Pure Math., vol. 28, Amer. Math. Soc., Providence, R.I., 1976. MR 0434781 (55:7745)
  • [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).

Similar Articles

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

American Mathematical Society