Here we list some of the logical symbols we use in the paper, for the benefit of readers who aren't used to symbolism at all, or are used to different symbols. Connectives bind according to their order in the table below, being the strongest. The scope of a quantifier, lambda-abstraction or descriptor extends as far to the right of the dot as possible. For example x. P[x] Q[x] R[x] is parsed as x. ((P[x] Q[x]) R[x]). We make a fuss about this last point because some books adopt the opposite convention.

Symbol	Other notations	English reading
	F, 0	false
	T, 1	true
P	~ P, -P	not P
P Q	P & Q, P . Q, P Q	P and Q
P Q	P | Q, P or Q, P + Q	P or Q
P Q	P Q, P Q	P implies Q
P Q	P Q, P ~ Q	P if and only if Q
x. P	( x) P, x:P, (x):P, x:P	for all x, P
x. P	( x) P, x:P, (Ex):P, x:P	there exists an x such that P
x. P	x.: P	some x such that P
x. P		the unique x such that P
x. t	x t, [x] t	the function of x which yields t
P	P	P is deducible (in a formal system) from

---

John Harrison 1996/8/13; HTML by 1996/8/16