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

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

Dem.

${\begin{aligned}&\scriptstyle {\left[*2\cdot 67{\frac {\sim p}{p}}\right]\vdash :.p\supset q.\supset .q:\supset .\sim p\supset q\qquad \qquad \qquad (1)}\\&\scriptstyle {\vdash .(1).*2\cdot 54.\supset \vdash .{\text{Prop}}}\end{aligned}}$

*2·69.⁠$\scriptstyle {\vdash :.p\supset q.\supset .q:\supset :q\supset p.\supset .p\qquad \left[*2\cdot 68.{\text{Perm}}.*2\cdot 62{\frac {q,p}{p,q}}\right]}$

*2·73.⁠$\scriptstyle {\vdash :.p\supset q.\supset :p\lor q\lor r.\supset .q\lor r\qquad [*2\cdot 621\cdot 38]}$

*2·74.⁠$\scriptstyle {\vdash :.q\supset p.\supset :p\lor q\lor r.\supset .p\lor r\qquad \left[*2\cdot 73{\frac {q,p}{p,q}}.{\text{Assoc}}.{\text{Syll}}\right]}$

*2·75.⁠$\scriptstyle {\vdash ::p\lor q.\supset :.p.\lor .q\supset r:\supset .p\lor r\qquad \left[*2\cdot 74{\frac {\sim q}{q}}.*2\cdot 53\cdot 31\right]}$

*2·76.⁠$\scriptstyle {\vdash :.p.\lor .q\supset r:\supset :p\lor q.\supset .p\lor r\qquad [*2\cdot 75.{\text{Comm}}]}$

*2·77.⁠$\scriptstyle {\vdash :.p.\supset .q\supset r:\supset :p\supset q.\supset .p\supset r\qquad \left[*2\cdot 76{\frac {\sim p}{p}}\right]}$

*2·8.⁠$\scriptstyle {\vdash :.q\lor r.\supset :\sim r\lor s.\supset .q\lor s}$

Dem.

${\begin{array}{ll}\scriptstyle {\vdash .*2\cdot 53.{\text{Perm}}.\supset \vdash :.q\lor r.}&\scriptstyle {\supset :\sim r\supset q:}\\\scriptstyle {[*2\cdot 38]}&\scriptstyle {\supset :\sim r\lor s.\supset .q\lor s:.\supset \vdash .{\text{Prop}}}\end{array}}$

*2·81.⁠$\scriptstyle {\vdash ::q.\supset .r\supset s:\supset :.p\lor q.\supset :p\lor r.\supset .p\lor s}$

Dem.

${\begin{array}{lll}\scriptstyle {\vdash .{\text{Sum}}.\supset \vdash ::q.\supset .r\supset s:\supset :.p\lor }&\scriptstyle {q.\supset :p.\lor .r\supset s\qquad \qquad }&\scriptstyle {(1)}\\\scriptstyle {\vdash .*2\cdot 76.{\text{Syll}}.\supset \vdash ::p\lor q.\supset :p.\lor }&\scriptstyle {.r\supset s:.\supset :.}\\&\scriptstyle {p\lor q.\supset :p\lor r.\supset .p\lor s}&\scriptstyle {(2)}\\\scriptstyle {\vdash .(1).(2).\supset \vdash .{\text{Prop}}}\end{array}}$

*2·82.⁠${\begin{aligned}\scriptstyle {\vdash :.p\lor q\lor r.\supset :p\lor \sim r\lor s.\supset .p\lor }&\scriptstyle {q\lor s}\\&\scriptstyle {\left[*2\cdot 8.*2\cdot 81{\frac {q\lor r,\sim r\lor s,q\lor s}{q,\quad r,\quad s}}\right]}\end{aligned}}$

*2·83.⁠${\begin{aligned}\scriptstyle {\vdash ::p.\supset .q\supset r:\supset :.p.\supset .r\supset s:}&\scriptstyle {\supset :p.\supset .q\supset s}\\&\scriptstyle {\left[*2\cdot 82{\frac {\sim p,\sim q}{p,~~q}}\right]}\end{aligned}}$

*2·85.⁠$\scriptstyle {\vdash :.p\lor q.\supset .p\lor r:\supset :p.\lor .q\supset r}$

Dem.

${\begin{array}{lllll}\scriptstyle {[{\text{Add}}.{\text{Syll}}]}&\scriptstyle {\vdash :.p\lor q}&\scriptstyle {.\supset .r:\supset .q\supset r}&&\scriptstyle {(1)}\\\scriptstyle {\vdash .*2\cdot 55.\supset }&\scriptstyle {\vdash ::\sim p.}&\scriptstyle {\supset :.p\lor r.\supset .r:.}\\\scriptstyle {[{\text{Syll}}]}&&\scriptstyle {\supset :.p\lor q.\supset .p\lor r:}&\scriptstyle {\supset :p\lor q.\supset .r:.}\\\scriptstyle {[(1).*2\cdot 83]}&&\scriptstyle {\supset :.p\lor q.\supset .p\lor r:}&\scriptstyle {\supset :q\supset r}&\scriptstyle {(2)}\\\scriptstyle {\vdash .(2).{\text{Com}}}&\scriptstyle {{\text{m}}.\supset \vdash :.}&\scriptstyle {\quad p\lor q.\supset .p\lor r:}&\scriptstyle {\supset :\sim p.\supset .q\supset r:}\\\scriptstyle {[*2\cdot 54]}&&&\scriptstyle {\supset :p.\lor .q\supset r:.\supset \vdash .}&\scriptstyle {\text{Prop}}\end{array}}$

*2·86.⁠$\scriptstyle {\vdash :.p\supset q.\supset .p\supset r:\supset :p.\supset .q\supset r\quad \left[*2\cdot 85{\frac {\sim p}{p}}\right]}$