*5·1. ⊢: p . q . ⊃ . p ≡ q {\displaystyle \scriptstyle {\vdash :p.q.\supset .p\equiv q}} [ ∗ 3 ⋅ 4 ⋅ 22 ] {\displaystyle \scriptstyle {[*3\cdot 4\cdot 22]}}
*5·11. ⊢: p ⊃ q . ∨ . ∼ p ⊃ q {\displaystyle \scriptstyle {\vdash :p\supset q.\lor .\sim p\supset q}} [ ∗ 2 ⋅ 51 ⋅ 54 ] {\displaystyle \scriptstyle {[*2\cdot 51\cdot 54]}}
*5·12. ⊢: p ⊃ q . ∨ . p ⊃∼ q {\displaystyle \scriptstyle {\vdash :p\supset q.\lor .p\supset \sim q}} [ ∗ 2 ⋅ 52 ⋅ 54 ] {\displaystyle \scriptstyle {[*2\cdot 52\cdot 54]}}
*5·13. ⊢: p ⊃ q . ∨ . q ⊃ p {\displaystyle \scriptstyle {\vdash :p\supset q.\lor .q\supset p}} [ ∗ 2 ⋅ 5 ⋅ 21 ] {\displaystyle \scriptstyle {[*2\cdot 5\cdot 21]}}
*5·14. ⊢: p ⊃ q . ∨ . q ⊃ r {\displaystyle \scriptstyle {\vdash :p\supset q.\lor .q\supset r}} [ Simp . Transp . ∗ 2 ⋅ 21 ] {\displaystyle \scriptstyle {[{\text{Simp}}.{\text{Transp}}.*2\cdot 21]}}
*5·15. ⊢: p ≡ q . ∨ . p ≡∼ q {\displaystyle \scriptstyle {\vdash :p\equiv q.\lor .p\equiv \sim q}}
Dem.
⊢ . ∗ 4 ⋅ 61. ⊃⊢:∼ ( p ⊃ q ) . ⊃ . p . ∼ q . [ ∗ 5 ⋅ 1 ] ⊃ . p ≡∼ q : [ ∗ 2 ⋅ 54 ] ⊃⊢: p ⊃ q . ∨ . p ≡∼ q (1) ⊢ . ∗ 4 ⋅ 61. ⊃⊢:∼ ( q ⊃ p ) . ⊃ . q . ∼ p . [ ∗ 5 ⋅ 1 ] ⊃ . q ≡∼ p . [ ∗ 4 ⋅ 12 ] ⊃ . p ≡∼ q : [ ∗ 2 ⋅ 54 ] ⊃⊢: q ⊃ p . ∨ . p ≡∼ q (2) ⊢ . ( 1 ) . ( 2 ) . ∗ 4 ⋅ 41. ⊃⊢ . Prop {\displaystyle {\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. ⊢ . ∼ ( p ≡ q . p ≡∼ q ) {\displaystyle \scriptstyle {\vdash .\sim (p\equiv q.p\equiv \sim q)}}
⊢ . ∗ 3 ⋅ 26. ⊃⊢: p ≡ q . p ⊃∼ q . ⊃ . p ⊃ q . p ⊃∼ q . [ ∗ 4 ⋅ 82 ] ⊃ . ∼ p (1) ⊢ . ∗ 3 ⋅ 27. ⊃⊢: p ≡ q . p ⊃∼ q . ⊃ . q ⊃ p . p ⊃∼ q . [ Syll ] ⊃ . q ⊃∼ q . [ Abs ] ⊃ . ∼ q (2) ⊢ . ( 1 ) . ( 2 ) . Comp . ⊃⊢: p ≡ q . p ⊃∼ q . ⊃ . ∼ p . ∼ q . [ ∗ 4 ⋅ 65 q , p p , q ] ⊃ . ∼ ( ∼ q ⊃ p ) (3) ⊢ . ( 3 ) . Exp . ⊃⊢: . p ≡ q . ⊃: p ⊃∼ q . ⊃ . ∼ ( ∼ q ⊃ p ) : [ Id . ( ∗ 1 ⋅ 01 ) ] ⊃:∼ ( p ⊃∼ q ) . ∨ . ∼ ( ∼ q ⊃ p ) : [ ∗ 4 ⋅ 51. ( ∗ 4 ⋅ 01 ) ] ⊃:∼ ( p ≡∼ q ) : . ⊃⊢ . Prop {\displaystyle {\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. ⊢: p ∨ q . ∼ ( p . q ) . ≡ . p ≡∼ q {\displaystyle \scriptstyle {\vdash :p\lor q.\sim (p.q).\equiv .p\equiv \sim q}}
⊢ . ∗ 4 ⋅ 64 ⋅ 21. ⊃⊢: p ∨ q . ≡ . ∼ q ⊃ p (1) ⊢ . ∗ 4 ⋅ 63. Transp . ⊃⊢:∼ ( p . q ) . ≡ . p ⊃∼ q (2) ⊢ . ( 1 ) . ( 2 ) . ∗ 4 ⋅ 38 ⋅ 21. ⊃⊢ . Prop {\displaystyle {\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}}}
![{\displaystyle \scriptstyle {[*3\cdot 4\cdot 22]}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b9d9c71710aea5f2dc91d235c005c57c09a93c59)
![{\displaystyle \scriptstyle {[*2\cdot 51\cdot 54]}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cc116caae51d658d4731acdbef99e060a954bfb4)
![{\displaystyle \scriptstyle {[*2\cdot 52\cdot 54]}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d115c7ea091ddfa42e7e371017072ee9249b9ddd)
![{\displaystyle \scriptstyle {[*2\cdot 5\cdot 21]}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/34cb52f3f0207c082fccce374b7197f2bdfdc464)
![{\displaystyle \scriptstyle {[{\text{Simp}}.{\text{Transp}}.*2\cdot 21]}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a466b7b2255b5590805d581b0624074c9e1e5a3d)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/41fa552d633603c41a74927d866b1e3dd6dc8cbc)
![{\displaystyle {\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}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/576eb02eeb97343098873491253e88986c255731)
