left up


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, not 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 forallx. P[x] and Q[x] implies R[x] is parsed as forallx. ((P[x] and Q[x]) implies R[x]). We make a fuss about this last point because some books adopt the opposite convention.

SymbolOther notationsEnglish reading
bottom F, 0 false
top T, 1 true
not P ~ P, -P not P
P and Q P & Q, P . Q, P Q P and Q
P or Q P | Q, P or Q, P + Q P or Q
P implies Q P fun Q, P prsupset Q P implies Q
P iff Q P iff Q, P ~ Q P if and only if Q
forallx. P (forall x) P, forall x:P, (x):P, andl x:P for all x, P
existsx. P (exists x) P, exists x:P, (Ex):P, orl x:P there exists an x such that P
epsilonx. P tau x.: P some x such that P
iotax. P   the unique x such that P
lambdax. t x mapsto t, [x] t the function of x which yields t
Gamma |- P Gamma fun P P is deducible (in a formal system) from Gamma

left right up home John Harrison 1996/8/13; HTML by 1996/8/16