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

proposition $\scriptstyle {q\supset p.r\supset p.\supset .q\lor r\supset p}$, where $\scriptstyle {p}$ is $\scriptstyle {(\exists z).\phi z}$. Now it will be found, on referring to *4.77 and the propositions used in its proof, that this proposition depends upon *1.2, i.e. $\scriptstyle {p\lor p.\supset .p}$. Hence it cannot be used by us to prove $\scriptstyle {(\exists x).\phi x.\lor .(\exists x).\phi x:\supset .(\exists x).\phi x}$, and thus we are compelled to assume the primitive proposition *9.11.

We have next two propositions concerned with inference to or from propositions containing apparent variables, as opposed to implication. First, we have, for the new meaning of implication resulting from the above definitions of negation and disjunction, the analogue of *1.1, namely *9.12. What is implied by a true premiss is true. Pp.

That is to say, given "$\scriptstyle {\vdash .p}$" and "$\scriptstyle {\vdash .p\supset q}$," we may proceed to "$\scriptstyle {\vdash .q}$," even when the propositions $\scriptstyle {p}$ and $\scriptstyle {q}$ are not elementary. Also, as in *1.11, we may proceed from "$\scriptstyle {\vdash .\phi x}$" and "$\scriptstyle {\vdash .\phi x\supset \psi x}$" to "$\scriptstyle {\vdash .\psi x}$," where $\scriptstyle {x}$ is a real variable, and $\scriptstyle {\phi }$ and $\scriptstyle {\psi }$ are not necessarily elementary functions. It is in this latter form that the axiom is usually needed. It is to be assumed for functions of several variables as well as for functions of one variable.

We have next the primitive proposition which permits the passage from a real to an apparent variable, namely "when $\scriptstyle {\phi y}$ may be asserted, where $\scriptstyle {y}$ may be any possible argument, then $\scriptstyle {(x).\phi x}$ may be asserted." In other words, when $\scriptstyle {\phi y}$ is true however $\scriptstyle {y}$ may be chosen among possible arguments, then $\scriptstyle {(x).\phi x}$ is true, i.e. all values of $\scriptstyle {\phi }$ are true. That is to say, if we can assert a wholly ambiguous value $\scriptstyle {\phi y}$, that must be because all values are true. We may express this primitive proposition by the words: "What is true in any case, however the case may be selected, is true in all cases." We cannot symbolise this proposition, because if we put

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

that means: "However $\scriptstyle {y}$ may be chosen, $\scriptstyle {\phi y}$ implies $\scriptstyle {(x).\phi x}$," which is in general false. What we mean is: "If $\scriptstyle {\phi y}$ is true however $\scriptstyle {y}$ may be chosen, then $\scriptstyle {(x).\phi x}$ is true." But we have not supplied a symbol for the mere hypothesis of what is asserted in "$\scriptstyle {\vdash .\phi y}$," where $\scriptstyle {y}$ is a real variable, and it is not worth while to supply such a symbol, because it would be very rarely required. If, for the moment, we use the symbol $\scriptstyle {\lbrack \phi y\rbrack }$ to express this hypothesis, then our primitive proposition is

$\scriptstyle {\vdash :\lbrack \phi y\rbrack .\supset .(x).\phi x}$ Pp.

In practice, this primitive propositions is only used for inference, not for implication; that is to say, when we actually have an assertion containing a real variable, it enables us to turn this real variable into an apparent variable by placing it in brackets immediately after the assertion-sign, followed by enough dots to reach to the end of the assertion. This process will be called "turning a real variable into an apparent variable." Thus we may assert our primitive proposition, for technical use, in the form: