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

*4·4.⁠$\scriptstyle {\vdash :.p.q\lor r.\equiv :p.q.\lor .p.r}$

*4·41.⁠$\scriptstyle {\vdash :p\lor .q.r:\equiv .p\lor q.p\lor r}$

The second of these forms has no analogue in ordinary algebra.

*4·71.⁠$\scriptstyle {\vdash :.p\supset q.\equiv :p.\equiv .p.q}$

I.e. $\scriptstyle {p}$ implies $\scriptstyle {q}$ when, and only when, $\scriptstyle {p}$ is equivalent to $\scriptstyle {p.q}$. This proposition is used constantly; it enables us to replace any implication by an equivalence.

*4·73.⁠$\scriptstyle {\vdash :.q.\supset :p.\equiv .p.q}$

I.e. a true factor may be dropped from or added to a proposition without altering the truth-value of the proposition.

---

• 4·01.⁠$\scriptstyle {p\equiv q.=.p\supset q.q\supset p\quad {\text{Df}}}$

*4·02.⁠$\scriptstyle {p\equiv q\equiv r.=.p\equiv q.q\equiv r\quad {\text{Df}}}$

This definition serves merely to provide a convenient abbreviation.

• 4·1.⁠$\scriptstyle {\vdash :p\supset q.\equiv .\sim q\supset \sim p}$$\scriptstyle {[*2\cdot 16\cdot 17]}$

• 4·11.⁠$\scriptstyle {\vdash :p\equiv q.\equiv .\sim p\equiv \sim q}$$\scriptstyle {[*2\cdot 16\cdot 17.*3\cdot 47\cdot 22]}$

*4·12.⁠$\scriptstyle {\vdash :p\equiv \sim q.\equiv .q\equiv \sim p}$$\scriptstyle {[*2\cdot 03\cdot 15]}$

• 4·13.⁠$\scriptstyle {\vdash .p\equiv \sim (\sim p)}$$\scriptstyle {[*2\cdot 12\cdot 14]}$

*4·14.⁠$\scriptstyle {\vdash :.p.q.\supset .r:\equiv :p.\sim r.\supset .\sim q}$$\scriptstyle {[*3\cdot 37.*4\cdot 13]}$

*4·15.⁠$\scriptstyle {\vdash :.p.q.\supset .\sim r:\equiv :q.r.\supset .\sim p}$$\scriptstyle {[*3\cdot 22.*4\cdot 13\cdot 14]}$

• 4·2.⁠$\scriptstyle {\vdash .p\equiv p}$$\scriptstyle {[{\text{Id}}.*3\cdot 2]}$

• 4·21.⁠$\scriptstyle {\vdash :p\equiv q.\equiv .q\equiv p}$$\scriptstyle {[*3\cdot 22]}$

• 4·22.⁠$\scriptstyle {\vdash :p\equiv q.q\equiv r.\supset .p\equiv r}$

Dem.

${\begin{array}{lllr}\scriptstyle {\vdash .*3\cdot 26.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .p\equiv q.}\\\scriptstyle {[*3\cdot 26]}&&\scriptstyle {\supset .p\supset q\qquad }&\scriptstyle {(1)}\\\scriptstyle {\vdash .*3\cdot 27.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .q\equiv r.}\\\scriptstyle {[*3\cdot 26]}&&\scriptstyle {\supset .q\supset r}&\scriptstyle {(2)}\\\scriptstyle {\vdash .(1).(2).*2\cdot 83.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .p\supset r}&\scriptstyle {(3)}\\\scriptstyle {\vdash .*3\cdot 27.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .q\equiv r.}\\\scriptstyle {[*3\cdot 27]}&&\scriptstyle {\supset .r\supset q}&\scriptstyle {(4)}\\\scriptstyle {\vdash .*3\cdot 26.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .p\equiv q.}\\\scriptstyle {[*3\cdot 27]}&&\scriptstyle {\supset .q\supset p}&\scriptstyle {(5)}\\\scriptstyle {\vdash .(4).(5).*2\cdot 83.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .r\supset p}&\scriptstyle {(6)}\\\scriptstyle {\vdash .(3).(6).{\text{Comp}}.}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}$