6.2.2. Bound variables

When a variable in an abstractor does appear in the body, its occurrences in the body are said to be bound to the abstractor. If a variable is in the scope of more than one abstractor containing it, it is bound to the one with narrowest scope. When a variable is not in the scope of an abstractor that lists it, it is not bound and is said to be free. In particular, when an expression like x² + 3xy + 1 or x introduced x to y is considered by itself outside the context of an abstract, all variables in it are free.

Variables have the grammatical status of individual terms but have no definite reference values. In the context of a formula like x² + 3xy + 1, free variables are naturally thought of as variable quantities (hence their name). As they vary in their reference, the value of the formula varies as a result. When variables are bound in an abstract like [x² + 3xy + 1]_xy, there is no longer this sort of variation. The abstract makes a fixed reference to a mathematical object, a polynomial function, that incorporates the variation within itself. Because of this, an older terminology referred to bound variables as apparent variables.

The notation for predicates and functors used in 6.1 can be thought as a variation on the notation for abstracts that responds to the apparent character of bound variables by removing them entirely. We understand a bracketed sentence- or individual-term-with-blanks to represent an abstract in which each of the blanks is filled with a different variable and the variables appear in the same order in the body and the abstactor. So [ _ introduced _ to _ ] would come to the same thing as the abstract

Because the blanks in the English expression correspond one for one and in the same order to the places of the predicate or functor, there is nothing for bound variables to indicate.

Bracketing alone is not sufficient in cases where the places of a predicate do not correspond one for one to the blanks, but a notation clearer than bound variables might replace the misleading appearance variable terms by a more direct indication of the correspondence between blanks and places that the variables mark—e.g., by lines linking places locations in the body with places in the abstractor, as in the following alternative notation for the predicate abstract [x introduced x to y]_xy.

Here, lines show how blanks in the body of the abstract correspond to places of the predicate. In the abstract using variables, the same thing is indicated by the correspondence between the variables marking blanks in the body and with the list of variables in the abstractor.

Because bound variables only mark a correspondence between locations in the body of the abstract and the abstactor, the bound variables of different abstracts have no connection with one another. This means that, for example, the following abstracts express the same predicate:

Each says that for any input terms τ and υ (in that order), the output sentence should be τ introduced τ to υ.

We will refer to as alphabetic variants expressions, like these, that use different variables to indicate the same correspondence between blanks in the body and places for input. Not only can alphabetic variants use different variables to express the same meaning, the significance of a given variable will vary from abstract to abstract; and this can happen even when the abstracts are alphabetic variants. For example, although the variable y appears in both of the abstracts above, it would be replaced by a different one of the input terms in each case.

The body of a predicate abstract is grammatically like a sentence even though it may contain free variables. It is standard to speak of an expression as closed if any variables it contains are bound and call an expression open if it contains free variables. Logicians typically use the term formula for any expression that is grammatically like a sentence whether it is open or closed, and reserve the term sentence for closed formulas. Since all formulas are grammatically like sentences, the grammatical vocabulary applied to sentences in previous chapters applies to all formulas. For example, formulas can be built from formulas by use of connectives, so formulas can be compound and have components. The label (individual) term will be used for both open and closed expressions with the latter distinguished simply as closed terms.

It is time to update our notion of atomic sentences or, more generally, atomic formulas. Now that we analyze sentences and other formulas into components like predicates and individual terms, the atomic formulas will no longer be simply the unanalyzed sentences though those will still count as atomic. We will now also count as atomic any predication. Although predications are compound and can even have formulas as components (though not as immediate components), their role in derivations is sufficiently analogous to that of unanalyzed sentences for it to make sense to put them both in the same category. This analogy lies behind our use of capital letters for predicates, and it can be built into our syntactic categories: an unanalyzed sentence can be thought of as a zero-place predicate, one that requires no input to yield a sentence as output.