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

of the type of the argument $\scriptstyle {x}$ in $\scriptstyle {\chi (x,y,z,\ldots )}$, and therefore both $\scriptstyle {\phi x}$ and $\scriptstyle {\psi x}$ take arguments of the same type. Hence, in such a case, if both $\scriptstyle {\phi x}$ and $\scriptstyle {\psi x}$ can be asserted, so can $\scriptstyle {\phi x.\psi x}$.

As an example of the use of this proposition, take the proof of *3·47. We there prove and

${\begin{array}{lr}\scriptstyle {\vdash :.p\supset r.q\supset s.\supset :p.q.\supset .q.r\qquad \qquad }&\scriptstyle {(1)}\\\scriptstyle {\vdash :.p\supset r.q\supset s.\supset :q.r.\supset .r.s}&\scriptstyle {(2)}\end{array}}$

and what we wish to prove is

$\scriptstyle {p\supset r.q\supset s.\supset :p.q.\supset .r.s}$,

which is *3·47. Now in (1) and (2), $\scriptstyle {p}$, $\scriptstyle {q}$, $\scriptstyle {r}$, $\scriptstyle {s}$ are elementary propositions (as everywhere in Section A); hence by *1·7·71, applied repeatedly, "$\scriptstyle {p\supset r.q\supset r.\supset :p.q.\supset .q.r}$" and "$\scriptstyle {p\supset r.q\supset s.\supset :q.r.\supset .r.s}$" are elementary propositional functions. Hence by *3·03, we have

$\scriptstyle {\vdash ::p\supset r.q\supset s.\supset :p.q.\supset .q.r:.p\supset r.q\supset s.\supset :q.r.\supset .r.s}$,

whence the result follows by *3·43 and *3·33.

The principal propositions of the present number are the following:

*3·2.⁠$\scriptstyle {\vdash :.p.\supset :q.\supset .p.q}$

I.e. "$\scriptstyle {p}$ implies that $\scriptstyle {q}$ implies $\scriptstyle {p.q}$," i.e. if each of two propositions is true, so is their logical product.

*3·26.⁠$\scriptstyle {\vdash :p.q.\supset .p}$

*3·27.⁠$\scriptstyle {\vdash :p.q.\supset .q}$

I.e. if the logical product of two propositions is true, then each of the two propositions severally is true.

*3·3.⁠$\scriptstyle {\vdash :.p.q.\supset .r:\supset :p.\supset .q\supset r}$

I.e. if $\scriptstyle {p}$ and $\scriptstyle {q}$ jointly imply $\scriptstyle {r}$, then $\scriptstyle {p}$ implies that $\scriptstyle {q}$ implies $\scriptstyle {r}$. This principle (following Peano) will be called "exportation," because $\scriptstyle {q}$ is "exported" from the hypothesis. It will be referred to as "Exp."

*3·31.⁠$\scriptstyle {\vdash :.p.\supset .q\supset r:\supset :p.q.\supset .r}$

This is the correlative of the above, and will be called (following Peano) "importation" (referred to as "Imp").

*3·35.⁠$\scriptstyle {\vdash :p.p\supset q.\supset .q}$

I.e. "if $\scriptstyle {p}$ is true, and $\scriptstyle {q}$ follows from it, then $\scriptstyle {q}$ is true." This will be called the "principle of assertion" (referred to as "Ass"). It differs from *1·1 by the fact that it does not apply only when $\scriptstyle {p}$ really is true, but requires merely the hypothesis that $\scriptstyle {p}$ is true.

*3·43.⁠$\scriptstyle {\vdash :.p\supset q.p\supset r.\supset :p.\supset .q.r}$

I.e. if a proposition implies each of two propositions, then it implies their logical product. This is called by Peano the "principle of composition." It will be referred to as "Comp."