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

*4·6. $\scriptstyle {\vdash :\qquad ~p\supset q.\equiv .\sim p\lor q}$$\scriptstyle {[*4\cdot 2.(*1\cdot 01)]}$

*4·61.$\scriptstyle {\vdash :\quad \,\sim (p\supset q).\equiv .p.\sim q}$$\scriptstyle {[*4\cdot 6\cdot 11\cdot 52]}$

*4·62.$\scriptstyle {\vdash :\quad ~~p\supset \sim q.\equiv .\sim p\lor \sim q}$$\scriptstyle {\left[*4\cdot 6{\frac {\sim q}{q}}\right]}$

*4·63.$\scriptstyle {\vdash :~~\sim (p\supset \sim q).\equiv .p.q}$$\scriptstyle {[*4\cdot 62\cdot 11\cdot 5]}$

*4·64.$\scriptstyle {\vdash :\quad ~~\sim p\supset q.\equiv .p\lor q}$$\scriptstyle {[*2\cdot 53\cdot 54]}$

*4·65.$\scriptstyle {\vdash :~~\sim (\sim p\supset q).\equiv .\sim p.\sim q}$$\scriptstyle {[*4\cdot 64\cdot 11\cdot 56]}$

*4·66.$\scriptstyle {\vdash :\quad \,\sim p\supset \sim q.\equiv .p\lor \sim q}$$\scriptstyle {\left[*4\cdot 64{\frac {\sim q}{q}}\right]}$

*4·67.$\scriptstyle {\vdash :\sim (\sim p\supset \sim q).\equiv .\sim p.q}$$\scriptstyle {[*4\cdot 66\cdot 11\cdot 54]}$

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

Dem.

${\begin{array}{llr}\scriptstyle {\vdash .*3\cdot 27.{\text{Syll}}.}&\scriptstyle {\supset \vdash :.p.\supset .p.q:\supset .p\supset q}&\scriptstyle {\quad (1)}\\\scriptstyle {\vdash .{\text{Comp}}}&\scriptstyle {\supset \vdash :.p\supset .p.p\supset q.\supset :p.\supset .p.q:.}\\\scriptstyle {[{\text{Exp}}]}&\scriptstyle {\supset \vdash ::p\supset p.\supset :.p\supset q.\supset :p.\supset .p.q::}\\\scriptstyle {[{\text{Id}}]}&\scriptstyle {\supset \vdash :.p\supset q.\supset :p.\supset .p.q}&\scriptstyle {(2)}\\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {\vdash .{\text{Prop}}}\end{array}}$

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

Dem.

${\begin{array}{llr}\scriptstyle {\vdash .*3\cdot 21.}&\scriptstyle {\supset \vdash ::p.q.\supset .p:\supset :.p.\supset .p.q:\supset :p.\equiv .p.q::}\\\scriptstyle {[*3\cdot 26]}&\scriptstyle {\supset \vdash :.p.\supset .p.q:\supset :p.\equiv .p.q}&\scriptstyle {(1)}\\\scriptstyle {\vdash .*3\cdot 26.}&\scriptstyle {\supset \vdash :.p.\equiv .p.q:\supset :p.\supset .p.q}&\scriptstyle {(2)}\\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {\supset \vdash :.p.\supset .p.q:\equiv :p.\equiv .p.q}&\scriptstyle {(3)}\\\scriptstyle {\vdash .(3).*4\cdot 7\cdot 22.}&\scriptstyle {\vdash .{\text{Prop}}}\end{array}}$

The above proposition is constantly used. It enables us to transform every implication into an equivalence, which is an advantage if we wish to assimilate symbolic logic as far as possible to ordinary algebra. But when symbolic logic is regarded as an instrument of proof, we need implications, and it is usually inconvenient to substitute equivalences. Similar remarks apply to the following proposition.

*4·72.$\scriptstyle {\vdash :.p\supset q.\equiv :q.\equiv .p\lor q}$

Dem.

${\begin{array}{ll}\scriptstyle {\vdash .*4\cdot 1.\supset \vdash :.p\supset q.}&\scriptstyle {\equiv :\sim q\supset \sim p:}\\\scriptstyle {\left[*4\cdot 71{\frac {\sim q,\sim p}{p,~~q}}\right]}&\scriptstyle {\equiv :\sim q.\equiv .\sim q.\sim p:}\\\scriptstyle {[*4\cdot 12]}&\scriptstyle {\equiv :q.\equiv .\sim (\sim q.\sim p):}\\\scriptstyle {[4\cdot 57]}&\scriptstyle {\equiv :q.\equiv .q\lor p:}\\\scriptstyle {[*4\cdot 31]}&\scriptstyle {\equiv :q.\equiv .p\lor q:.\supset \vdash .{\text{Prop}}}\end{array}}$