Consider Consider (*| R:P).

Any occurrence of the variable x which appears in R or P is said to be in the scope of the quantification over x. An occurence of x which is in the scope of a quantification over x is said to be a bound occurrence. An occurence of a variable x which is not in the scope of any quantification over x is said to be a free occurrence.

If the variable x does occur free in the expression P we write
x dnof in P, or following the text,  occurs(`x,`P).

Look at
k+(+k | 1 k 6:k2).

The k's which appear in 1 k 6 and k2 are in the scope of the quantification over k and are bound occurrences of k. The k which appears to the left of the + is not in the scope of any quantification over k and is a free occurrence of k.

You can see that the k's are different by considering k+(+k | 1 k 6:k2) for universe of discourse N. We obtain
k+(12 + 22 + 32 + 42 + 52 + 62)
and the freely occurring k is the only occurrence of k which remains.


File translated from TEX by TTH, version 2.60.
On 3 Nov 2000, 12:00.