Abstract

This paper begins the study of first-order functions, which are a generalization of truth-functions. The concepts of truth-table and systems of truth-functions, both introduced in propositional logic by Post, are also generalized and studied in the quantificational setting. The general facts about these concepts are given in the first five sections, and constitute a “general theory” of first-order functions. The central theme of this paper is the relation of definition among notions expressed by formulas of first-order logic. We emphasize that logic is not concerned only with the consequence relation among notions expressed by formulas. It also attends to the relation of definition among notions, where a notion is defined from other notions. Sections 5 and 6 deal exclusively with the relation of definition among notions expressed by formulas of first-order logic. In these sections, we study the systems of first-order functions, which are the sets of first-order functions closed under definitions. Sections 7 and 8 are concerned with the relativization of first-order functions to a class of structures. The relativization to a class of structures is a fundamental operation which is used in order to relate the theory of first-order functions with set theory and first-order model theory, a subject which we have barely scratched the surface. The apparatus developed in this paper enables us to define what is a vehicle for the foundation of classical mathematics in set theory, and, in Sect. 8, we prove that first-order logic with one binary predicate variable is not a minimal vehicle for the foundation of classical mathematics in set theory. Sections 9 and 10 introduce further operations and ideals of first-order functions. Besides some results on the influence of the arguments of a first-order function, a result about definability is proved in Sect. 10.1. It is this theorem that provides necessary and sufficient conditions for a first-order function to be in a finitely generated ideal. In Sect. 11, this result is applied to the problem of predicate definability in classes of structures, the problem with which Beth’s theorem dealt in the case of elementary classes