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. Binary connectives bind according to their order in the
table below, being the strongest.
The scope of a quantifier, lambda-abstraction or descriptor is 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. The
table below gives the symbolic expressions we will use.
Symbol | Other notations | English reading |
![]() | F, 0 | false |
![]() | T, 1 | true |
![]() | ~ P, -P | not P |
P ![]() | P & Q, P . Q, P Q | P and Q |
P ![]() | P | Q, P or Q, P + Q | P or Q |
P ![]() | P
![]() ![]() | P implies Q |
P ![]() | P ~ Q, P
![]() | P if and only if Q |
![]() | (![]() ![]() ![]() | for all x, P |
![]() | (![]() ![]() ![]() | there exists an x such that P |
![]() | some x such that P | |
![]() | ![]() | the unique x such that P |
![]() | x ![]() | the function of x which yields t |
![]() | P is deducible (in a formal system) | |