SECTION A ]
EQUIVALENCE AND FORMAL RULES
125
*4·43.
⊢:
.
p
.
≡:
p
∨
q
.
p
∨
∼
q
{\displaystyle \scriptstyle {\vdash :.p.\equiv :p\lor q.p\lor \sim q}}
Dem.
⊢
.
∗
2
⋅
2.
⊃⊢:
p
.
⊃
.
p
∨
q
:
p
.
⊃
.
p
∨
∼
q
:
[
Comp
]
⊃⊢:
p
.
⊃
.
p
∨
q
.
p
∨
∼
q
(
1
)
⊢
.
∗
2
⋅
65
∼
p
p
.
⊃⊢:
.
∼
p
⊃
q
.
⊃:∼
p
⊃∼
q
.
⊃
.
p
:
.
[
Imp
]
⊃⊢:
.
∼
p
⊃
q
.
∼
p
⊃∼
q
.
⊃
.
p
:
.
[
∗
2
⋅
53.
∗
3
⋅
47
]
⊃⊢:
.
p
∨
q
.
p
∨
∼
q
.
⊃
.
p
(
2
)
⊢
.
(
1
)
.
(
2
)
.
⊃⊢
.
Prop
{\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .*2\cdot 2.}&\scriptstyle {\supset \vdash :p.\supset .p\lor q:p.\supset .p\lor \sim q:}\\\scriptstyle {[{\text{Comp}}]}&\scriptstyle {\supset \vdash :p.\supset .p\lor q.p\lor \sim q}&\scriptstyle {\qquad (1)}\\\scriptstyle {\vdash .*2\cdot 65{\frac {\sim p}{p}}.}&\scriptstyle {\supset \vdash :.\sim p\supset q.\supset :\sim p\supset \sim q.\supset .p:.}\\\scriptstyle {[{\text{Imp}}]}&\scriptstyle {\supset \vdash :.\sim p\supset q.\sim p\supset \sim q.\supset .p:.}\\\scriptstyle {[*2\cdot 53.*3\cdot 47]}&\scriptstyle {\supset \vdash :.p\lor q.p\lor \sim q.\supset .p}&\scriptstyle {(2)}\\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}}
*4·44.
⊢:
.
p
.
≡:
p
.
∨
.
p
.
q
{\displaystyle \scriptstyle {\vdash :.p.\equiv :p.\lor .p.q}}
Dem.
⊢
.
∗
2
⋅
2.
⊃⊢:
.
p
.
⊃:
p
.
∨
.
p
.
q
(
1
)
⊢
.
Id
.
∗
3
⋅
26.
⊃⊢:
.
p
⊃
p
:
p
.
q
.
⊃
.
p
:
.
[
∗
3
⋅
44
]
⊃⊢:
.
p
.
∨
.
p
.
q
:⊃
.
p
(
2
)
⊢
.
(
1
)
.
(
2
)
.
⊃⊢
.
Prop
{\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .*2\cdot 2.}&\scriptstyle {\supset \vdash :.p.\supset :p.\lor .p.q}&\scriptstyle {\qquad (1)}\\\scriptstyle {\vdash .{\text{Id}}.*3\cdot 26.}&\scriptstyle {\supset \vdash :.p\supset p:p.q.\supset .p:.}\\\scriptstyle {[*3\cdot 44]}&\scriptstyle {\supset \vdash :.p.\lor .p.q:\supset .p}&\scriptstyle {(2)}\\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}}
*4·45.
⊢:
p
.
≡
.
p
.
p
∨
q
[
∗
3
⋅
26.
∗
2
⋅
2
]
{\displaystyle \scriptstyle {\vdash :p.\equiv .p.p\lor q\quad [*3\cdot 26.*2\cdot 2]}}
The following formulae are due to De Morgan, or rather, are the propositional analogues of formulae given by De Morgan for classes. The first of them, it will be observed, merely embodies our definition of the logical product.
*4·5.
⊢:
p
.
q
.
≡
.
∼
(
∼
p
∨
∼
q
)
{\displaystyle \scriptstyle {\vdash :\qquad \,p.q.\equiv .\sim (\sim p\lor \sim q)}}
[
∗
4
⋅
2.
(
∗
3
⋅
01
)
]
{\displaystyle \scriptstyle {[*4\cdot 2.(*3\cdot 01)]}}
*4·51.
⊢:
∼
(
p
.
q
)
.
≡
.
∼
p
∨
∼
q
{\displaystyle \scriptstyle {\vdash :\quad \,\sim (p.q).\equiv .\sim p\lor \sim q}}
[
∗
4
⋅
5
⋅
12
]
{\displaystyle \scriptstyle {[*4\cdot 5\cdot 12]}}
*4·52.
⊢:
p
.
∼
q
.
≡
.
∼
(
∼
q
∨
q
)
{\displaystyle \scriptstyle {\vdash :\quad ~~p.\sim q.\equiv .\sim (\sim q\lor q)}}
[
∗
4
⋅
5
∼
q
q
.
∗
4
⋅
13
]
{\displaystyle \scriptstyle {\left[*4\cdot 5{\frac {\sim q}{q}}.*4\cdot 13\right]}}
*4·53.
⊢:
∼
(
p
.
∼
q
)
.
≡
.
∼
p
∨
q
{\displaystyle \scriptstyle {\vdash :~\,\sim (p.\sim q).\equiv .\sim p\lor q}}
[
∗
4
⋅
52
⋅
12
]
{\displaystyle \scriptstyle {[*4\cdot 52\cdot 12]}}
*4·54.
⊢:
∼
p
.
q
.
≡
.
∼
(
p
∨
∼
q
)
{\displaystyle \scriptstyle {\vdash :\quad ~\,\sim p.q.\equiv .\sim (p\lor \sim q)}}
[
∗
4
⋅
5
∼
p
p
.
∗
4
⋅
13
]
{\displaystyle \scriptstyle {\left[*4\cdot 5{\frac {\sim p}{p}}.*4\cdot 13\right]}}
*4·55.
⊢:
∼
(
∼
p
.
q
)
.
≡
.
p
∨
∼
q
{\displaystyle \scriptstyle {\vdash :~\,\sim (\sim p.q).\equiv .p\lor \sim q}}
[
∗
4
⋅
54
⋅
12
]
{\displaystyle \scriptstyle {[*4\cdot 54\cdot 12]}}
*4·56.
⊢:
∼
p
.
∼
q
.
≡
.
∼
(
p
∨
q
)
{\displaystyle \scriptstyle {\vdash :~~~\,\sim p.\sim q.\equiv .\sim (p\lor q)}}
[
∗
4
⋅
54
∼
q
q
.
∗
4
⋅
13
]
{\displaystyle \scriptstyle {\left[*4\cdot 54{\frac {\sim q}{q}}.*4\cdot 13\right]}}
*4·57.
⊢:∼
(
∼
p
.
∼
q
)
.
≡
.
p
∨
q
{\displaystyle \scriptstyle {\vdash :\sim (\sim p.\sim q).\equiv .p\lor q}}
[
∗
4
⋅
56
⋅
12
]
{\displaystyle \scriptstyle {[*4\cdot 56\cdot 12]}}
The following formulae are obtained immediately from the above. They are important as showing how to transform implications into sums or into denials of products, and vice versa. It will be observed that the first of them merely embodies the definition *1·01 .