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

true." This is a true proposition, but it holds equally when $\scriptstyle {p}$ is not true and when $\scriptstyle {p}$ does not imply $\scriptstyle {q}$. It does not, like the principle we are concerned with, enable us to assert $\scriptstyle {q}$ simply, without any hypothesis. We cannot express the principle symbolically, partly because any symbolism in which $\scriptstyle {p}$ is variable only gives the hypothesis that $\scriptstyle {p}$ is true, not the fact that it is true^[1].

The above principle is used whenever we have to deduce a proposition from a proposition. But the immense majority of the assertions in the present work are assertions of propositional functions, i.e. they contain an undetermined variable. Since the assertion of a propositional function is a different primitive idea from the assertion of a proposition, we require a primitive proposition different from *1·1, though allied to it, to enable us to deduce the assertion of a propositional function "$\scriptstyle {\psi x}$" from the assertions of the two propositional functions "$\scriptstyle {\phi x}$" and "$\scriptstyle {\phi x\supset \psi x}$." This primitive proposition is as follows:

*1·11. When $\scriptstyle {\phi x}$ can be asserted, where $\scriptstyle {x}$ is a real variable, and $\scriptstyle {\phi x\supset \psi x}$ can be asserted, where $\scriptstyle {x}$ is a real variable, then $\scriptstyle {\psi x}$ can be asserted, where $\scriptstyle {x}$ is a real variable. $\scriptstyle {\text{Pp.}}$

This principle is also to be assumed for functions of several variables.

Part of the importance of the above primitive proposition is due to the fact that it expresses in the symbolism a result following from the theory of types, which requires symbolic recognition. Suppose we have the two assertions of propositional functions "$\scriptstyle {\vdash .\phi x}$" and "$\scriptstyle {\vdash .\phi x\supset \psi x}$"; then the "$\scriptstyle {x}$" in $\scriptstyle {\phi x}$ is not absolutely anything, but anything for which as argument the function "$\scriptstyle {\phi x}$" is significant; similarly in "$\scriptstyle {\phi x\supset \psi x}$" the $\scriptstyle {x}$ is anything for which "$\scriptstyle {\phi x\supset \psi x}$" is significant. Apart from some axiom, we do not know that the $\scriptstyle {x}$'s for which "$\scriptstyle {\phi x\supset \psi x}$" is significant are the same as those for which "$\scriptstyle {\phi x}$" is significant. The primitive proposition *1·11, by securing that, as the result of the assertions of the propositional functions "$\scriptstyle {\phi x}$" and "$\scriptstyle {\phi x\supset \psi x}$," the propositional function $\scriptstyle {\psi x}$ can also be asserted, secures partial symbolic recognition, in the form most useful in actual deductions, of an important principle which follows from the theory of types, namely that, if there is any one argument $\scriptstyle {a}$ for which both "$\scriptstyle {\phi a}$" and "$\scriptstyle {\psi a}$" are significant, then the range of arguments for which "$\scriptstyle {\phi x}$" is significant is the same as the range of arguments for which "$\scriptstyle {\psi x}$" is significant. It is obvious that, if the propositional function "$\scriptstyle {\phi x\supset \psi x}$" can be asserted, there must be arguments $\scriptstyle {a}$ for which "$\scriptstyle {\phi a\supset \psi a}$" is significant, and for which, therefore, "$\scriptstyle {\phi a}$" and "$\scriptstyle {\psi a}$" must be significant. Hence, by our principle, the values of $\scriptstyle {x}$ for which "$\scriptstyle {\phi x}$" is significant are the same as those for which "$\scriptstyle {\psi x}$" is significant, i.e. the type of possible arguments for $\scriptstyle {\phi {\hat {x}}}$ (cf. p. 15) is the same as that of possible arguments for $\scriptstyle {\psi {\hat {x}}}$. The

1. For further remarks on this principle, cf. Principles of Mathematics, § 38.