Principia mathematica, by Alfred North Whitehead ... and Bertrand Russell.

180

MATHEMATICAL LOGIC

[PART I

*13'22. F: (Liz, w). z = x. w = y. O (z, w). =. ( (x, y)
Demn.
F.*11 55. D F:. (az,v ).z= x.w=y. (z,w).
=: (az): Z = x: (aw). W =y. p (z, w):
[*13'195] -: (w).w=y.((x,w):
[*13-195]: (x, y):.:) F. Prop
This proposition is the analogue, for two variables, of *13'195. It is
frequently used, especially in the theory of couples (*54, *55, *56).
The following proposition is useful in the theory of types. Its purpose is
to show that, if a is any argument for which "Oa" is significant, i.e. for
which we have Qa v~i a, then " fx" is significant when, and only when, x is
either identical with a or not identical with a. It follows (as will be proved
in *20'81) that, if "ba" and "*a" are both significant, the class of values
of x for which " Jx" is significant is the same as the class of those for which
"xx" is significant, i.e. two types which have a common member are identical.
In the following proof, the chief point to observe is the use of *10'221.
There are two variables, a and x, to be identified. In the first use, we depend
upon the fact that Oa and x=a both occur in both (4) and (5): the occurrence
of ba in both justifies the identification of the two a's, and when these have
been identified, the occurrence of x = a in both justifies the identification of
the two x's. (Unless the a's had been already identified, this would not be
legitimate, because "x = a" is typically ambiguous if neither x nor a is of
given type.) The second use of *10'221 is justified by the fact that both Oa
and fix occur in both (2) and (6).
*13'3. F:: Oa v-Oa. D:. fx v x:.: x= a. v. x a
Dem..*211.. QDh..vbx (1)
F. (1). Simp. ) F: Qfa v-Oa. D. x ve~x (2)
F.*211. D: x= a. v. xv a (3)
F. (3). Simp. D:. bavna. ): x= a. v. x = a (4)
F. *13'101. Comm. D F:. Oa v ~a. D: x = a. D. O.x v bx (5)
F. (4). (5). *10-13-221.
F:: sa v~,c. D: =a. v. x + a:.,av,a.: x= a. D. z vx(6 (6)
F. (2). (6). *10-1 3221. )
F:: Oa v a-a. x v-:. ax vv Oa:. a: vx= a.:. v. a:.
Oa v- ~a. D: ' = a.:). Ox; v, -. x (7)
F. (7). Simp. ):: a v a.. 'z v ~:. )a v ~-.: x= a. v. x a (8)
F. (8). *5'35. ):: v V-Oa. F:. Ocx v x D:x. -: x = a. v. x = a::
D - Prop