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

*2·13.⁠$\scriptstyle {\vdash .p\lor \sim \{\sim (\sim p)\}}$

This proposition is a lemma for *2·14, which, with *2·12, constitutes the principle of double negation.

Dem.

${\begin{array}{lll}\scriptstyle {\left[{\text{Sum}}{\frac {\sim p,\sim \{\sim (\sim p)\}}{q,~~~~~~r}}\right]\quad }&\scriptstyle {\vdash :.\sim p.\supset .\sim \{\sim (\sim p)\}.\supset :}&\\&\scriptstyle {\qquad p\lor \sim p.\supset .p\lor \sim \{\sim (\sim p)\}\qquad }&\scriptstyle {(1)}\\\scriptstyle {\left[*2\cdot 12{\frac {\sim p}{p}}\right]}&\scriptstyle {\vdash :\sim p.\supset .\sim \{\sim (\sim p)\}}&\scriptstyle {(2)}\\\scriptstyle {[(1).(2).*1\cdot 11]}&\scriptstyle {\vdash :p\lor \sim p.\supset .p\lor \sim \{\sim (\sim p)\}}&\scriptstyle {(3)}\\\scriptstyle {[(3).*2\cdot 11.*1\cdot 11]}&\scriptstyle {\vdash :p\lor \sim \{\sim (\sim p)\}}&\end{array}}$

*2·14.⁠$\scriptstyle {\vdash .\sim (\sim p)\supset p}$

Dem.

${\begin{array}{lll}\scriptstyle {\left[{\text{Perm}}{\frac {\sim \{\sim (\sim p)\}}{q}}\right]\quad }&\scriptstyle {\vdash :p\lor \sim \{\sim (\sim p)\}.\supset .\sim \{\sim (\sim p)\}\lor p\qquad }&\scriptstyle {(1)}\\\scriptstyle {[(1).*2\cdot 13.*1\cdot 11]}&\scriptstyle {\vdash .\sim \{\sim (\sim p)\}\lor p}&\scriptstyle {(2)}\\\scriptstyle {[(2).(*1\cdot 01)]}&\scriptstyle {\vdash .\sim (\sim p)\supset p}&\end{array}}$

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

Dem.

${\begin{array}{lll}\scriptstyle {\left[*2\cdot 05{\frac {\sim p,\sim (\sim q)}{p,~~~~~~r}}\right]\quad }&\scriptstyle {\vdash :.q\supset \sim (\sim q).\supset :\sim p\supset q.\supset .\sim p\supset \sim (\sim q)\qquad }&\scriptstyle {~(1)}\\\scriptstyle {\left[*2\cdot 12{\frac {q}{p}}\right]}&\scriptstyle {\vdash .q\supset \sim (\sim q)}&\scriptstyle {~(2)}\\\scriptstyle {[(1).(2).*1\cdot 11]}&\scriptstyle {\vdash :\sim p\supset q.\supset .\sim p\supset \sim (\sim q)}&\scriptstyle {~(3)}\\\scriptstyle {\left[*2\cdot 03{\frac {\sim p,\sim q}{p,~~q}}\right]}&\scriptstyle {\vdash :\sim p\supset \sim (\sim q).\supset .\sim q\supset \sim (\sim p)}&\scriptstyle {~(4)}\\\scriptstyle {\left[*2\cdot 05{\frac {\sim q,\sim (\sim p),p}{p,~~q,~~r}}\right]}&\scriptstyle {\vdash :.\sim (\sim p)\supset p.\supset :\sim q\supset \sim (\sim p).\supset .\sim q\supset p}&\scriptstyle {~(5)}\\\scriptstyle {[(5).*2\cdot 14.*1\cdot 11]}&\scriptstyle {\vdash :\sim q\supset \sim (\sim p).\supset .\sim q\supset p}&\scriptstyle {~(6)}\\\scriptstyle {\left[*2\cdot 05{\frac {\sim p\supset q,\sim p\supset \sim (\sim q),\sim q\supset \sim (\sim p)}{p,~~~~~~q,~~~~~~r}}\right]}&\scriptstyle {\vdash ::}&\\&\scriptstyle {\quad \sim p\supset \sim (\sim q).\supset .\sim q\supset \sim (\sim p):\supset :.}&\\&\scriptstyle {\quad \sim p\supset q.\supset .\sim p\supset \sim (\sim q):\supset :\sim p\supset q.\supset .\sim q\supset \sim (\sim p)}&\scriptstyle {~(7)}\\\scriptstyle {[(4).(7).*1\cdot 11]}&\scriptstyle {\vdash :.\sim p\supset q.\supset .\sim p\supset \sim (\sim q):\supset :}&\\&\scriptstyle {\sim p\supset q.\supset .\sim q\supset \sim (\sim p)}&\scriptstyle {~(8)}\\\end{array}}$