Page:Russell, Whitehead - Principia Mathematica, vol. I, 1910.djvu/160

*9.13. In any assertion containing a real variable, this real variable may be turned into an apparent variable of which all possible values are asserted to satisfy the function in question. Pp.

We have next two primitive propositions concerned with types. These require some preliminary explanations.

Primitive Idea: Individual. We say that $\scriptstyle {x}$ is "individual" if $\scriptstyle {x}$ is neither a proposition nor a function (cf. pp. 53, 54).

*9.131. Definition of "being of the same type." The following is a step-by-step definition, the definition for higher types presupposing that for lower types. We say that $\scriptstyle {u}$ and $\scriptstyle {v}$ "are of the same type" if (1) both are individuals, (2) both are elementary functions taking arguments of the same type, (3) $\scriptstyle {u}$ is a function and $\scriptstyle {v}$ is its negation, (4) $\scriptstyle {u}$ is $\scriptstyle {\phi {\hat {x}}}$ or $\scriptstyle {\psi {\hat {x}}}$, and $\scriptstyle {v}$ is $\scriptstyle {\phi {\hat {x}}\lor \phi {\hat {x}}}$, where $\scriptstyle {\phi {\hat {x}}}$ and $\scriptstyle {\psi {\hat {x}}}$ are elementary functions, (5) $\scriptstyle {u}$ is $\scriptstyle {(y).\phi ({\hat {x}},y)}$ and $\scriptstyle {v}$ is $\scriptstyle {(z).\psi ({\hat {x}},z)}$, where $\scriptstyle {\phi ({\hat {x}},{\hat {y}})}$, $\scriptstyle {\psi ({\hat {x}},{\hat {y}})}$ are of the same type, (6) both are elementary propositions, (7) $\scriptstyle {u}$ is a proposition and $\scriptstyle {v}$ is $\scriptstyle {\sim u}$, or (8) $\scriptstyle {u}$ is $\scriptstyle {(x).\phi x}$ and $\scriptstyle {v}$ is $\scriptstyle {(y).\psi y}$, where $\scriptstyle {\phi {\hat {x}}}$ and $\scriptstyle {\psi {\hat {x}}}$ are of the same type.

Our primitive propositions are:

*9.14. If "$\scriptstyle {\phi x}$" is significant, the if $\scriptstyle {x}$ is of the same type as $\scriptstyle {a}$, "$\scriptstyle {\phi a}$" is significant, and vice versa. Pp. (Cf. note on *10.121, p.146.)

*9.15. If, for some $\scriptstyle {a}$ there is a proposition $\scriptstyle {\phi a}$, then there is a function $\scriptstyle {\phi {\hat {x}}}$, and vice versa. Pp.

It will be seen that, in virtue of the definitions,

$\scriptstyle {(x).\phi x.\supset .p}$ means $\scriptstyle {\sim (x).\phi x.\lor .p}$, i.e. $\scriptstyle {(\exists x).\sim \phi x.\lor .p}$,

i.e. $\scriptstyle {\exists x).\sim \phi x\lor p}$, i.e. $\scriptstyle {(\exists x).\phi x\supset p}$

$\scriptstyle {(\exists x).\phi x.\supset .p}$ means $\scriptstyle {\sim (\exists x).\phi x.\lor .p}$, i.e. $\scriptstyle {(x).\sim \phi x.\lor .p}$,

i.e. $\scriptstyle {(x).\sim \phi x\lor p}$, i.e $\scriptstyle {(x).\phi x\supset p}$

In order to prove that $\scriptstyle {(x).\phi x}$ and $\scriptstyle {(\exists x).\phi x}$ obey the same rules of deduction as $\scriptstyle {\phi x}$, we have to prove that propositions of the forms $\scriptstyle {(x).\phi x}$ and $\scriptstyle {(\exists x).\phi x}$ may replace one ore more of the propositions $\scriptstyle {p}$, $\scriptstyle {q}$, $\scriptstyle {r}$ in *1.2–.6. When this has been proved, the previous proofs of subsequent propositions in *2–*5 become applicable. These proofs are given below. Certain other propositions, required in the proofs, are also proved.

*9.2. $\scriptstyle {\vdash :(x).\phi x.\supset .\phi y}$

The aboce proposition states the principle of deduction from the general to the particular, i.e. "what holds in all cases, holds in any one case."

Dem.

${\begin{array}{llr}\scriptstyle {\vdash *2.1.\supset \vdash .\sim \phi y\lor \phi y}&&\qquad \scriptstyle {\text{(1)}}\\\scriptstyle {\vdash .*9.1.\supset \vdash :\sim \phi y\lor \phi y.\supset .(\exists x).\sim \phi x\lor \phi y}&&\qquad \scriptstyle {\text{(2)}}\\\scriptstyle {\vdash .{\text{(1)}}.{\text{(2)}}.*1.11.\supset }&\scriptstyle {\vdash .(\exists x).\sim \phi x\lor \phi y}&\qquad \scriptstyle {\text{(3)}}\\\scriptstyle {[{\text{(3)}}.(*9.05)]}&\scriptstyle {\vdash :(\exists x).\sim \phi x.\lor .\phi y}&\qquad \scriptstyle {\text{(4)}}\\\scriptstyle {[{\text{(4)}}.(*9.01.*1.01)]}&\scriptstyle {\vdash :(x).\phi x.\supset .\phi y}\end{array}}$