Section A]
Equivalence and Formal Rules
127
*4·73.
⊢:
.
q
.
⊃:
p
.
≡
.
p
.
q
[
Simp
.
∗
4
⋅
71
]
{\displaystyle \scriptstyle {\vdash :.q.\supset :p.\equiv .p.q\quad [{\text{Simp}}.*4\cdot 71]}}
This proposition is very useful, since it shows that a true factor may be omitted from a product without altering its truth or falsehood, just as a true hypothesis may be omitted from an implication.
*4·74.
⊢:
.
∼
p
.
⊃:
q
.
≡
.
p
∨
q
{\displaystyle \scriptstyle {\vdash :.\sim p.\supset :q.\equiv .p\lor q}}
[
∗
2
⋅
21.
∗
4
⋅
72
]
{\displaystyle \scriptstyle {[*2\cdot 21.*4\cdot 72]}}
*4·76.
⊢:
.
p
⊃
q
.
p
⊃
r
.
≡:
p
.
⊃
.
q
.
r
{\displaystyle \scriptstyle {\vdash :.p\supset q.p\supset r.\equiv :p.\supset .q.r}}
[
∗
4
⋅
41
∼
p
p
.
(
∗
1
⋅
01
)
]
{\displaystyle \scriptstyle {\left[*4\cdot 41{\frac {\sim p}{p}}.(*1\cdot 01)\right]}}
*4·77.
⊢:
.
q
⊃
p
.
r
⊃
p
.
≡:
q
∨
r
.
⊃
.
p
{\displaystyle \scriptstyle {\vdash :.q\supset p.r\supset p.\equiv :q\lor r.\supset .p}}
[
∗
3
⋅
44.
Add
.
∗
2
⋅
2
]
{\displaystyle \scriptstyle {[*3\cdot 44.{\text{Add}}.*2\cdot 2]}}
*4·78.
⊢:
.
p
⊃
q
.
∨
.
p
⊃
r
:≡:
p
.
⊃
.
q
∨
r
{\displaystyle \scriptstyle {\vdash :.p\supset q.\lor .p\supset r:\equiv :p.\supset .q\lor r}}
Dem.
⊢
.
∗
4
⋅
2.
(
∗
1
⋅
01
)
.
⊃⊢:
.
p
⊃
q
.
∨
.
p
⊃
r
:
≡:∼
p
∨
q
.
∨
.
∼
p
∨
r
:
[
∗
4
⋅
33
]
≡
.
∼
p
.
∨
.
q
∨
∼
p
∨
r
:
[
∗
4
⋅
31
⋅
37
]
≡:∼
p
.
∨
.
∼
p
∨
q
∨
r
:
[
∗
4
⋅
33
]
≡:∼
p
∨
∼
p
.
∨
.
q
∨
r
:
[
∗
4
⋅
25
⋅
37
]
≡:∼
p
.
∨
.
q
∨
r
:
[
∗
4
⋅
2.
(
∗
1
⋅
01
)
]
≡:
p
.
⊃
.
q
∨
r
:
.
⊃⊢
.
Prop
{\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .*4\cdot 2.(*1\cdot 01).\supset \vdash :.p\supset q.\lor .p\supset r:}&\scriptstyle {\equiv :\sim p\lor q.\lor .\sim p\lor r:}\\\scriptstyle {[*4\cdot 33]}&\scriptstyle {\equiv .\sim p.\lor .q\lor \sim p\lor r:}\\\scriptstyle {[*4\cdot 31\cdot 37]}&\scriptstyle {\equiv :\sim p.\lor .\sim p\lor q\lor r:}\\\scriptstyle {[*4\cdot 33]}&\scriptstyle {\equiv :\sim p\lor \sim p.\lor .q\lor r:}\\\scriptstyle {[*4\cdot 25\cdot 37]}&\scriptstyle {\equiv :\sim p.\lor .q\lor r:}\\\scriptstyle {[*4\cdot 2.(*1\cdot 01)]}&\scriptstyle {\equiv :p.\supset .q\lor r:.\supset \vdash .{\text{Prop}}}\end{array}}}
*4·79.
⊢:
.
q
⊃
p
.
∨
.
r
⊃
p
:≡:
q
.
r
.
⊃
.
p
{\displaystyle \scriptstyle {\vdash :.q\supset p.\lor .r\supset p:\equiv :q.r.\supset .p}}
Dem.
⊢
.
∗
4
⋅
1
⋅
39.
⊃⊢:
.
q
⊃
p
.
∨
.
r
⊃
p
:
≡:∼
p
⊃∼
q
.
∨
.
∼
p
⊃∼
r
:
[
∗
4
⋅
78
]
≡:∼
p
.
⊃
.
∼
q
∨
∼
r
:
[
∗
2
⋅
15
]
≡:∼
(
∼
q
∨
∼
r
)
.
⊃
.
p
:
[
∗
4
⋅
2.
(
∗
3
⋅
01
)
]
≡:
q
.
r
.
⊃
.
p
:
.
⊃⊢
.
Prop
{\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .*4\cdot 1\cdot 39.\supset \vdash :.q\supset p.\lor .r\supset p:}&\scriptstyle {\equiv :\sim p\supset \sim q.\lor .\sim p\supset \sim r:}\\\scriptstyle {[*4\cdot 78]}&\scriptstyle {\equiv :\sim p.\supset .\sim q\lor \sim r:}\\\scriptstyle {[*2\cdot 15]}&\scriptstyle {\equiv :\sim (\sim q\lor \sim r).\supset .p:}\\\scriptstyle {[*4\cdot 2.(*3\cdot 01)]}&\scriptstyle {\equiv :q.r.\supset .p:.\supset \vdash .{\text{Prop}}}\end{array}}}
Note. The analogues, for classes, of *4·78·79 are false. Take, e.g. *4·78, and put
p
=
{\displaystyle \scriptstyle {p=}}
English people,
q
=
{\displaystyle \scriptstyle {q=}}
men,
r
=
{\displaystyle \scriptstyle {r=}}
women. Then
p
{\displaystyle \scriptstyle {p}}
is contained in
q
{\displaystyle \scriptstyle {q}}
or
r
{\displaystyle \scriptstyle {r}}
, but is not contained in
q
{\displaystyle \scriptstyle {q}}
and is not contained in
r
{\displaystyle \scriptstyle {r}}
.
*4·8.
⊢:
p
⊃∼
p
.
≡
.
∼
p
{\displaystyle \scriptstyle {\vdash :p\supset \sim p.\equiv .\sim p}}
[
∗
2
⋅
01.
Simp
]
{\displaystyle \scriptstyle {[*2\cdot 01.{\text{Simp}}]}}
*4·81.
⊢:∼
p
⊃
p
.
≡
.
p
{\displaystyle \scriptstyle {\vdash :\sim p\supset p.\equiv .p}}
[
∗
2
⋅
18.
Simp
]
{\displaystyle \scriptstyle {[*2\cdot 18.{\text{Simp}}]}}
*4·82.
⊢:
p
⊃
q
.
p
⊃∼
q
.
≡
.
∼
p
{\displaystyle \scriptstyle {\vdash :p\supset q.p\supset \sim q.\equiv .\sim p}}
[
∗
2
⋅
65.
Imp
.
∗
2
⋅
21.
Comp
]
{\displaystyle \scriptstyle {[*2\cdot 65.{\text{Imp}}.*2\cdot 21.{\text{Comp}}]}}
*4·83.
⊢:
p
⊃
q
.
∼
p
⊃
q
.
≡
.
q
{\displaystyle \scriptstyle {\vdash :p\supset q.\sim p\supset q.\equiv .q}}
[
∗
2
⋅
61.
Imp
.
Simp
.
Comp
]
{\displaystyle \scriptstyle {[*2\cdot 61.{\text{Imp}}.{\text{Simp}}.{\text{Comp}}]}}
Note. *4·82·83 may also be obtained from *4·43 , of which they are virtually other forms.
*4·84.
⊢:
.
p
≡
q
.
⊃:
p
⊃
r
.
≡
.
q
⊃
r
{\displaystyle \scriptstyle {\vdash :.p\equiv q.\supset :p\supset r.\equiv .q\supset r}}
[
∗
2
⋅
06.
∗
3
⋅
47
]
{\displaystyle \scriptstyle {[*2\cdot 06.*3\cdot 47]}}
*4·85.
⊢:
.
p
≡
q
.
⊃:
r
⊃
p
.
≡
.
r
⊃
q
{\displaystyle \scriptstyle {\vdash :.p\equiv q.\supset :r\supset p.\equiv .r\supset q}}
[
∗
2
⋅
05.
∗
3
⋅
47
]
{\displaystyle \scriptstyle {[*2\cdot 05.*3\cdot 47]}}
*4·86.
⊢:
.
p
≡
q
.
⊃:
p
≡
r
.
≡
.
q
≡
r
{\displaystyle \scriptstyle {\vdash :.p\equiv q.\supset :p\equiv r.\equiv .q\equiv r}}
[
∗
4
⋅
21
⋅
22
]
{\displaystyle \scriptstyle {[*4\cdot 21\cdot 22]}}
*4·87.
⊢:
.
p
.
q
.
⊃
.
r
:≡:
p
.
⊃
.
q
⊃
r
:≡:
q
.
⊃
.
p
⊃
r
:≡:
q
.
p
.
⊃
.
r
{\displaystyle \scriptstyle {\vdash :.p.q.\supset .r:\equiv :p.\supset .q\supset r:\equiv :q.\supset .p\supset r:\equiv :q.p.\supset .r}}
[
Exp
.
Comm
.
Imp
]
{\displaystyle \scriptstyle {[{\text{Exp}}.{\text{Comm}}.{\text{Imp}}]}}
*4·87 embodies in one proposition the principles of exportation and importation and the commutative principle.