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.