6.2.2. Bound variables

If a variable in an abstractor appears in the body of an abstract, its occurrences in the body are said to be bound to the abstractor. So any occurrence of x₁, …, x_n in the body --- of the following abstract is bound to the abstractor x₁…x_n:

If a variable is in the scope of more than one abstractor containing it, it is bound to the one with narrowest scope. So the first occurrence of x and the occurrence of y are bound to the abstractor xy in the following while both the occurrences of x outside the inner abstract and the occurrence of z within its body are bound to the abstractor xz:

A variable that is not bound to any abstractor is said to be free. So z is free in [y introduced x to z]_xy, and 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) since, when 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 reference to a mathematical object, a polynomial function, that incorporates the variation but does not itself vary. 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 of as a variation on the notation for abstracts that deals with the apparent character of bound variables by removing them entirely. We will 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 no need for bound variables to indicate the relation between the two.

Bracketing alone is not sufficient in cases where the places of a predicate do not correspond one for one to the blanks. However, we might supplement it by lines showing how places correspond to blanks.

This is clearer than the corresponding use of bound variables

but it is significantly less convenient. Still, it is worth bearing in mind, even when bound variables are used, since the lines in the graphical notation depict the pattern of binding of variables by 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 υ, and pattern of binding in each would be depicted in the same way in the graphical notation.

Expressions, like these, that use different variables to indicate the same correspondence between blanks in the body and places for input will be referred to as alphabetic variants. Notice that alphabetic variants can use a given variable in different ways. 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 within it and call an expression open if one or more of its variables is free. 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. In particular, formulas can be built from formulas by use of connectives, so formulas can be compound and have components.

The distinction between open and closed expressions applies to term-like expressions also, but the terminology is handled differently. Both open and closed expressions are classified as (individual) terms with closed expressions 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 any sentences that go unanalyzed will still count as atomic). We will now also count as atomic any predication. Predications are compound and can even have formulas as components (albeit not immediate components), but the role of predications 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.