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

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

*5·11.⁠$\scriptstyle {\vdash :p\supset q.\lor .\sim p\supset q}$$\scriptstyle {[*2\cdot 51\cdot 54]}$

*5·12.⁠$\scriptstyle {\vdash :p\supset q.\lor .p\supset \sim q}$$\scriptstyle {[*2\cdot 52\cdot 54]}$

*5·13.⁠$\scriptstyle {\vdash :p\supset q.\lor .q\supset p}$$\scriptstyle {[*2\cdot 5\cdot 21]}$

*5·14.⁠$\scriptstyle {\vdash :p\supset q.\lor .q\supset r}$$\scriptstyle {[{\text{Simp}}.{\text{Transp}}.*2\cdot 21]}$

*5·15.⁠$\scriptstyle {\vdash :p\equiv q.\lor .p\equiv \sim q}$

Dem.

${\begin{array}{lllr}\scriptstyle {\vdash .*4\cdot 61.}&\scriptstyle {\supset \vdash :\sim (p\supset q).}&\scriptstyle {\supset .p.\sim q.}\\\scriptstyle {[*5\cdot 1]}&&\scriptstyle {\supset .p\equiv \sim q:}\\\scriptstyle {[*2\cdot 54]}&\scriptstyle {\supset \vdash :p\supset q.\lor .p}&\scriptstyle {\equiv \sim q}&\scriptstyle {\qquad \qquad {\text{(1)}}}\\\scriptstyle {\vdash .*4\cdot 61.}&\scriptstyle {\supset \vdash :\sim (q\supset p).}&\scriptstyle {\supset .q.\sim p.}\\\scriptstyle {[*5\cdot 1]}&&\scriptstyle {\supset .q\equiv \sim p.}\\\scriptstyle {[*4\cdot 12]}&&\scriptstyle {\supset .p\equiv \sim q:}\\\scriptstyle {[*2\cdot 54]}&\scriptstyle {\supset \vdash :q\supset p.\lor .p}&\scriptstyle {\equiv \sim q}&\scriptstyle {\text{(2)}}\\\scriptstyle {\vdash .(1).(2)}&\scriptstyle {.*4\cdot 41.}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}$

*5·16.⁠$\scriptstyle {\vdash .\sim (p\equiv q.p\equiv \sim q)}$

Dem.

${\begin{array}{llr}\scriptstyle {\vdash .*3\cdot 26.\supset \vdash :p\equiv q.p\supset \sim q.}&\scriptstyle {\supset .p\supset q.p\supset \sim q.}\\\scriptstyle {[*4\cdot 82]}&\scriptstyle {\supset .\sim p}&\scriptstyle {\qquad \qquad {\text{(1)}}}\\\scriptstyle {\vdash .*3\cdot 27.\supset \vdash :p\equiv q.p\supset \sim q.}&\scriptstyle {\supset .q\supset p.p\supset \sim q.}\\\scriptstyle {[{\text{Syll}}]}&\scriptstyle {\supset .q\supset \sim q.}\\\scriptstyle {[{\text{Abs}}]}&\scriptstyle {\supset .\sim q}&\scriptstyle {\text{(2)}}\\\scriptstyle {\vdash .(1).(2).{\text{Comp}}.\supset \vdash :p\equiv q.p}&\scriptstyle {\supset \sim q.\supset .\sim p.\sim q.}\\\scriptstyle {\left[*4\cdot 65{\frac {q,p}{p,q}}\right]}&\scriptstyle {\supset .\sim (\sim q\supset p)}&\scriptstyle {\text{(3)}}\\\scriptstyle {\vdash .(3).{\text{Exp}}.\supset \vdash :.p\equiv q.\supset :p}&\scriptstyle {\supset \sim q.\supset .\sim (\sim q\supset p):}\\\scriptstyle {[{\text{Id}}.(*1\cdot 01)]}&\scriptstyle {\supset :\sim (p\supset \sim q).\lor .\sim (\sim q\supset p):}\\\scriptstyle {[*4\cdot 51.(*4\cdot 01)]}&\scriptstyle {\supset :\sim (p\equiv \sim q):.\supset \vdash .{\text{Prop}}}\end{array}}$

*5·17.⁠$\scriptstyle {\vdash :p\lor q.\sim (p.q).\equiv .p\equiv \sim q}$

Dem.

${\begin{array}{llr}\scriptstyle {\vdash .*4\cdot 64\cdot 21.}&\scriptstyle {\supset \vdash :p\lor q.\equiv .\sim q\supset p}&\scriptstyle {\qquad \qquad {\text{(1)}}}\\\scriptstyle {\vdash .*4\cdot 63.{\text{Transp}}.}&\scriptstyle {\supset \vdash :\sim (p.q).\equiv .p\supset \sim q}&\scriptstyle {\text{(2)}}\\\scriptstyle {\vdash .(1).(2).*4\cdot 38\cdot 21.}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}$