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

*5·18.$\scriptstyle {\vdash :p\equiv q.\equiv .\sim (p\equiv \sim q)}$$\scriptstyle {\left[*5\cdot 15\cdot 16.*5\cdot 17{\frac {p\equiv q,p\equiv \sim q}{p,\quad q}}\right]}$

*5·19.$\scriptstyle {\vdash .\sim (p\equiv \sim p)}$$\scriptstyle {\left[*5\cdot 18{\frac {p}{q}}.*4\cdot 2\right]}$

*5·21.$\scriptstyle {\vdash :\sim p.\sim q.\supset .p\equiv q}$$\scriptstyle {[*5\cdot 1.*4\cdot 11]}$

*5·22.$\scriptstyle {\vdash :.\sim (p\equiv q).\equiv :p.\sim q.\lor .q.\sim p}$$\scriptstyle {[*4\cdot 61\cdot 51\cdot 39]}$

*5·23.$\scriptstyle {\vdash :.p\equiv q.\equiv :p.q.\lor .\sim p.\sim q}$$\scriptstyle {\left[*5\cdot 18.*5\cdot 22{\frac {\sim q}{q}}.4\cdot 13\cdot 36\right]}$

*5·24.$\scriptstyle {\vdash :.\sim (p.q.\lor .\sim p.\sim q).\equiv :p.\sim q.\lor .q.\sim p}$$\scriptstyle {[*5\cdot 22\cdot 23]}$

*5·25.$\scriptstyle {\vdash :.p\lor q.\equiv :p\supset q.\supset .q}$$\scriptstyle {[*2\cdot 62\cdot 68]}$

From *5·25 it appears that we might have taken implication, instead of disjunction, as a primitive idea, and have defined "$\scriptstyle {p\lor q}$" as meaning "$\scriptstyle {p\supset q.\supset .q}$." This course, however, requires more primitive propositions than are required by the method we have adopted.

*5·3. $\scriptstyle {\vdash :.p.q.\supset .r:\equiv :p.q.\supset .p.r}$$\scriptstyle {[{\text{Simp}}.{\text{Comp}}.{\text{Syll}}]}$

*5·31.$\scriptstyle {\vdash :.r.p\supset q:\supset :p.\supset .q.r}$$\scriptstyle {[{\text{Simp}}.{\text{Comp}}]}$

*5·32.$\scriptstyle {\vdash :.p.\supset .q\equiv r:\equiv :p.q.\equiv .p.r}$$\scriptstyle {[*4\cdot 76.*3\cdot 3\cdot 31.*5\cdot 3]}$

This proposition is constantly required in subsequent proofs.

*5·33.$\scriptstyle {\vdash :.p.q\supset r.\equiv :p:p.q.\supset .r}$$\scriptstyle {[*4\cdot 73\cdot 84.*5\cdot 32]}$

*5·35.$\scriptstyle {\vdash :.p\supset q.p\supset r.\supset :p.\supset .q\equiv r}$$\scriptstyle {[{\text{Comp}}.*5\cdot 1]}$

*5·36.$\scriptstyle {\vdash :p.p\equiv q.\equiv .q.p\equiv q}$$\scriptstyle {[{\text{Ass}}.*4\cdot 38]}$

*5·4. $\scriptstyle {\vdash :.p.\supset .p\supset q:\equiv .p\supset q}$$\scriptstyle {[{\text{Simp}}.*2\cdot 43]}$

*5·41.$\scriptstyle {\vdash :.p\supset q.\supset .p\supset r:\equiv :p.\supset .q\supset r}$$\scriptstyle {[*2\cdot 77\cdot 86]}$

*5·42.$\scriptstyle {\vdash ::p.\supset .q\supset r:\equiv :.p.\supset :q.\supset .p.r}$$\scriptstyle {[*5\cdot 3.*4\cdot 87]}$

*5·44.$\scriptstyle {\vdash ::p\supset q.\supset :.p\supset r.\equiv :p.\supset .q.r}$$\scriptstyle {[*4\cdot 76.*5\cdot 3\cdot 32]}$

*5·5. $\scriptstyle {\vdash :.p.\supset :p\supset q.\equiv .q}$$\scriptstyle {[{\text{Ass}}.{\text{Exp}}.{\text{Simp}}]}$

*5·501.$\scriptstyle {\vdash :.p.\supset :q.\equiv .p\equiv q}$$\scriptstyle {[*5\cdot 1.{\text{Exp}}.{\text{Ass}}]}$

*5·53.$\scriptstyle {\vdash :.p\lor q\lor r.\supset .s:\equiv :p\supset s.q\supset s.r\supset s}$$\scriptstyle {[*4\cdot 77]}$

*5·54.$\scriptstyle {\vdash :.p.q.\equiv .p:\lor :p.q.\equiv .q}$$\scriptstyle {[*4\cdot 73.*4\cdot 44.{\text{Transp}}.*5\cdot 1]}$

*5·55.$\scriptstyle {\vdash :.p\lor q.\equiv .p:\lor :p\lor q.\equiv .q}$$\scriptstyle {[*1\cdot 3.*5\cdot 1.*4\cdot 74]}$

*5·6. $\scriptstyle {\vdash :.p.\sim q.\supset .r:\equiv :p.\supset .q\lor r}$$\scriptstyle {\left[*4\cdot 87{\frac {\sim q}{q}}.*4\cdot 64\cdot 85\right]}$

*5·61.$\scriptstyle {\vdash :p\lor q.\sim q.\equiv .p.\sim q}$$\scriptstyle {[*4\cdot 74.*5\cdot 32]}$

*5·62.$\scriptstyle {\vdash :.p.q.\lor .\sim q:\equiv .p\lor \sim q}$$\scriptstyle {\left[*4\cdot 7{\frac {q,p}{p,q}}\right]}$