Abstract
A variable binding term operator (vbto) is a non-logical
constant, say v, which combines with a variable y and a formula
F containing y free to form a term (vy:F) whose free
variables are exact ly those of F, excluding y.
Kalish-Montague proposed using vbtos to formalize definite descriptions, set abstracts {x: F}, minimalization in recursive function theory, etc. However, they gave no sematics for vbtos. Hatcher gave a semantics but one that has flaws. We give a correct semantic analysis of vbtos. We also give axioms for using them in deductions. And we conjecture strong completeness for the deductions with respect to the semantics. The conjecture was later proved independently by the authors and by Newton da Costa.
The expression (vy:F) is called a variable bound term (vbt). In case F has only
y free, (vy:F) has the syntactic propreties of an individual
constant; and under a suitable interpretation of the language
vy:F) denotes an individual. By a semantic analysis of vbtos
we mean a proposal for amending the standard notions of (1)
"an interpretation o f a first -order language" and (2) " the denotation
of a term under an interpretation and an assignment",
such that (1') an interpretation o f a first -order language associates
a set-theoretic structure with each vbto and (2') under
any interpretation and assignment each vb t denotes an individual.