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

that what holds of all, holds of any; for this would not be true if there were no "any."

(4) "If $\scriptstyle {\phi x}$ is always true, and $\scriptstyle {\psi x}$ is always true, then '$\scriptstyle {\phi x.\psi x}$' is always true," i.e.

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

(This requires that $\scriptstyle {\phi }$ and $\scriptstyle {\psi }$ should be functions which take arguments of the same type. We shall explain this requirement at a later stage.) The converse also holds; i.e. we have

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

It is to some extent optional which of the propositions connecting real and apparent variables are taken as primitive propositions. The primitive propositions assumed, on this subject, in the body of the work (*9), are the following:

(1)	$\scriptstyle {\vdash :\phi x.\supset .(\exists z).\phi z}$.
(2)	$\scriptstyle {\vdash :\phi x\lor \phi y.\supset .(\exists z).\phi z}$.

i.e. if either $\scriptstyle {\phi x}$ is true, or $\scriptstyle {\phi y}$ is true, then $\scriptstyle {(\exists z).\phi z}$ is true. (On the necessity for this primitive proposition, see remarks on *9·11 in the body of the work.)

(3) If we can assert $\scriptstyle {\phi y}$, where $\scriptstyle {y}$ is a real variable, then we can assert $\scriptstyle {(x).\phi x}$; i.e. what holds of any, however chosen, holds of all.

Formal implication and formal equivalence. When an implication, say $\scriptstyle {\phi x.\supset .\psi x}$, is said to hold always, i.e. when $\scriptstyle {(x):\phi x.\supset .\psi x}$, we shall say that $\scriptstyle {\phi x}$ formally implies $\scriptstyle {\psi x}$; and propositions of the form "$\scriptstyle {(x):\phi x.\supset .\psi x}$" will be said to state formal implications. In the usual instances of implication, such as "'Socrates is a man' implies 'Socrates is mortal,'" we have a proposition of the form "$\scriptstyle {\phi x.\supset .\psi x}$" in a case in which "$\scriptstyle {(x):\phi x.\supset .\psi x}$" is true. In such a case, we feel the implication as a particular case of a formal implication. Thus it has come about that implications which are not particular cases of formal implications have not been regarded as implications at all. There is also a practical ground for the neglect of such implications, for, speaking generally, they can only be known when it is already known either that their hypothesis is false or that their conclusion is true; and in neither of these cases do they serve to make us know the conclusion, since in the first case the conclusion need not be true, and in the second it is known already. Thus such implications do not serve the purpose for which implications are chiefly useful, namely that of making us know, by deduction, conclusions of which we were previously ignorant. Formal implications, on the contrary, do serve this purpose, owing to the psychological fact that we often know "$\scriptstyle {(x):\phi x.\supset .\psi x}$" and $\scriptstyle {\phi y}$, in cases where $\scriptstyle {\psi y}$ (which follows from these premisses) cannot easily be known directly.