Abstract
The purpose of the present paper is to prove a theorem on the possibility of reducing the question of deducibility of an arbitrary formula A in constructive predicate calculus with equality and functional symbols, to the question of the existence of a deducible formula in some sequence of quantifier-free formulas whose structure recalls the structure of the Herbrand developments [1] of the formula A. The concepts introduced in [2], which are connected with k-systems of Skolem functions and k-lexicons of formulas, will be utilized.
The main results of this note were presented to the Leningrad Seminar on Mathematical Logic on February 24, 1966.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Literature Cited
Herbrand, J., Recherches sur la theorie de la demonstration, Warsaw, 1930.
Mints, G E, ‘‘Choice of terms in quantifier rules of constructive predicate calculus,” this volume, p. 45.
Mints, G. E., “Herbrand theorem for predicate calculus with equality and functional symbols,” Doklady Akad. Nauk SSSR, 169(2):273–275 (1966).
Mints, G. E., “Skolem method of elimination of positive quantifiers in sequential calculi,” Doklady Akad. Nauk SSSR, 169(l):24–27 (1966).
Kreisel, G., Models, Translations and Interpretations. Mathematical Interpretations of Formal Systems, Amsterdam, 1965, pp. 26–50.
Editor information
Rights and permissions
Copyright information
© 1969 Consultants Bureau
About this chapter
Cite this chapter
Mints, G.E. (1969). Analog of Herbrand’s Theorem for Prenex Formulas of Constructive Predicate Calculus. In: Slisenko, A.O. (eds) Studies in Constructive Mathematics and Mathematical Logic. Seminars in Mathematics, vol 4. Springer, Boston, MA. https://doi.org/10.1007/978-1-4684-8968-2_12
Download citation
DOI: https://doi.org/10.1007/978-1-4684-8968-2_12
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4684-8970-5
Online ISBN: 978-1-4684-8968-2
eBook Packages: Springer Book Archive