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

to propositions of any type, and proceed as in *10, where the purely technical development is resumed.

It should be observed that although, in the present number, we prove that the analogues of the primitive proposition of *1, if they hold for proposition containing $\scriptstyle {n}$ apparent variables, also hold for such as contain $\scriptstyle {n+1}$, yet we must not suppose that mathematical induction may be used to infer that the analogues of the primitive proposition of *1 hold for propositions containing any number of apparent variables. Mathematical induction is a method of proof which is not yet applicable, and is (as will appear) incapable of being used freely until the theory of propositions containing apparent variables has been established. What we are enabled to do, by mean of the propositions in the present number, is to prove out desired result for any assigned number of apparent variables-say ten-by ten applications of the same proof. Thus we can prove, concerning any assigned proposition, that it obeys the analogues of the primitive propositions of *1, but we can only do this by proceeding set by step, not by any such compendious method as mathematical induction would afford. The fact that higher types can only be reached step by step is essential, since to proceed otherwise we should need an apparent variable which would wander from type to type, which would contradict the principle upon which types are built up.

---

Definition of Negation. We have first to define the negations of $\scriptstyle {(x).\phi x}$ and $\scriptstyle {(\exists x).\phi x}$. We define the negation of $\scriptstyle {(x).\phi x}$ as $\scriptstyle {(\exists x).\sim \phi x}$, i.e. "it is not the case that $\scriptstyle {\phi x}$ is always true" is to mean "it is the case that not-$\scriptstyle {\phi x}$ is sometimes true." Similarly the negation of $\scriptstyle {(\exists x).\phi x}$ is to be defined as $\scriptstyle {(x).\sim \phi x}$ Thus we put

*9.01. $\scriptstyle {\sim \lbrace (x).\phi x\rbrace .=.(\exists x).\sim \phi x}$ Df

*9.02. $\scriptstyle {\sim \lbrace (\exists x).\phi x\rbrace .=.(x).\sim \phi x}$ Df

To avoid brackets, we shell write $\scriptstyle {\sim (x).\phi x}$ in place of $\scriptstyle {\sim \lbrace (x).\phi x\lbrace }$, and $\scriptstyle {\sim (\exists x).\phi x}$ in place of $\scriptstyle {\sim \lbrace (\exists x).\phi x\rbrace }$. Thus;

*9.011. $\scriptstyle {\sim (x).\phi x.=.\sim \lbrace (x).\phi x\rbrace }$ Df

*9.021. $\scriptstyle {\sim (\exists x).\phi x.=.\sim \lbrace (\exists x).\phi x\rbrace }$ Df

Definition of Disjunction. To define disjunction when one or both of the propositions concerned is of the first order we have to distinguish six cases, as follow:

*9.03. $\scriptstyle {(x).\phi x.\lor .p:=.(x).\phi x\lor p}$ Df

*9.04. $\scriptstyle {p.\lor .(x).\phi x:=.(x).p\lor \phi x}$ Df

*9.05. $\scriptstyle {(\exists x).\phi x.\lor .p:=.(\exists x).\phi x\lor p}$ Df

*9.06. $\scriptstyle {p.\lor .(\exists x).\phi x:=.(\exists x).p\lor \phi x}$ Df

*9.07. $\scriptstyle {(x).\phi x.\lor .(\exists y).\psi y:=:(x):(\exists y).\phi x\lor \psi y}$ Df

*9.08. $\scriptstyle {(\exists y).\psi y.\lor .(x).\phi x:=:(x):(\exists y).\psi y\lor \phi x}$ Df