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

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

This principle shows that we may multiply both sides of an implication by a common factor; hence it is called by Peano the "principle of the factor." We shall refer to it as "Fact." It is the analogue, for multiplication, of the primitive proposition *1·6.

Dem.

${\begin{aligned}&{\begin{array}{ll}\scriptstyle {\vdash .{\text{Syll}}{\frac {\sim r}{r}}.\supset \vdash :.p\supset q.}&\scriptstyle {\supset :q\supset \sim r.\supset .p\supset \sim r:}\\\scriptstyle {[{\text{Transp}}]}&\scriptstyle {\supset :\sim (p\supset \sim r).\supset .\sim (q\supset \sim r):.}\end{array}}\\&\scriptstyle {~[{\text{Id}}.(*1\cdot 01.*3\cdot 01)]\supset \vdash .{\text{Prop}}}\end{aligned}}$

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

This proposition, or rather its analogue for classes, was proved by Leibniz, and evidently pleased him, since he calls it "præclarum theorema^[1]."

Dem.

${\begin{aligned}&{\begin{array}{llr}\scriptstyle {\vdash .*3\cdot 26.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :p\supset r:}\\\scriptstyle {[{\text{Fact}}]}&\scriptstyle {\supset :p.q.\supset .r.q:}\\\scriptstyle {[*3\cdot 22]}&\scriptstyle {\supset :p.q.\supset .q.r\qquad \qquad }&\scriptstyle {(1)}\\\scriptstyle {\vdash .*3\cdot 27.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :q\supset s:}\\\scriptstyle {[{\text{Fact}}]}&\scriptstyle {\supset :q.r.\supset .s.r:}\\\scriptstyle {[*3\cdot 22]}&\scriptstyle {\supset :q.r.\supset .r.s}&\scriptstyle {(2)}\end{array}}\\&\scriptstyle {~\vdash .(1).(2).*3\cdot 03.*2\cdot 83.\supset }\\&\scriptstyle {\qquad \qquad \vdash :.p\supset r.q\supset s.\supset :p.q.\supset .r.s:.\supset \vdash .{\text{Prop}}}\end{aligned}}$

*3·48.$\scriptstyle {\vdash :.p\supset r.q\supset s.\supset :p\lor q.\supset .r\lor s}$

This theorem is the analogue of *3·47.

Dem.

${\begin{aligned}&{\begin{array}{llr}\scriptstyle {\vdash .*3\cdot 26.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :p\supset r:}\\\scriptstyle {[{\text{Sum}}]}&\scriptstyle {\supset :p\lor q.\supset .r\lor q:}\\\scriptstyle {[{\text{Perm}}]}&\scriptstyle {\supset :p\lor q.\supset .q\lor r\qquad \qquad }&\scriptstyle {(1)}\\\scriptstyle {\vdash .*3\cdot 27.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :q\supset s:}\\\scriptstyle {[{\text{Sum}}]}&\scriptstyle {\supset :q\lor r.\supset .s\lor r:}\\\scriptstyle {[{\text{Perm}}]}&\scriptstyle {\supset :q\lor r.\supset .r\lor s}&\scriptstyle {(2)}\end{array}}\\&\scriptstyle {~\vdash .(1).(2).*2\cdot 83.\supset }\\&\scriptstyle {\qquad \qquad \vdash :.p\supset r.q\supset s.\supset :p\lor q.\supset .r\lor s:.\supset \vdash .{\text{Prop}}}\end{aligned}}$

1. Philosophical works, Gerhardt's edition, Vol. vii. p. 223.