SECTION A ]
IMMEDIATE CONSEQUENCES
109
*2·25.
⊢:
.
p
:
∨
:
p
∨
q
.
⊃
.
q
{\displaystyle \scriptstyle {\vdash :.p:\lor :p\lor q.\supset .q}}
Dem.
⊢
.
∗
2
⋅
1.
⊃⊢:∼
(
p
∨
q
)
.
∨
.
(
p
∨
q
)
:
[
Assoc
]
⊃⊢:
p
.
∨
.
{
∼
(
p
∨
q
)
.
∨
.
q
}
:⊃⊢
.
Prop
{\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .*2\cdot 1.}&\scriptstyle {\supset \vdash :\sim (p\lor q).\lor .(p\lor q):}\\\scriptstyle {[{\text{Assoc}}]}&\scriptstyle {\supset \vdash :p.\lor .\{\sim (p\lor q).\lor .q\}:\supset \vdash .{\text{Prop}}}\end{array}}}
*2·26.
⊢:
.
∼
p
:
∨
:
p
⊃
q
.
⊃
.
q
[
∗
2
⋅
25
∼
p
p
]
{\displaystyle \scriptstyle {\vdash :.\sim p:\lor :p\supset q.\supset .q\quad \left[*2\cdot 25{\frac {\sim p}{p}}\right]}}
*2·27.
⊢:
.
p
.
⊃:
p
⊃
q
.
⊃
.
q
[
∗
2
⋅
26
]
{\displaystyle \scriptstyle {\vdash :.p.\supset :p\supset q.\supset .q\quad [*2\cdot 26]}}
*2·3.
⊢:
p
∨
(
q
∨
r
)
.
⊃
.
p
∨
(
r
∨
q
)
{\displaystyle \scriptstyle {\vdash :p\lor (q\lor r).\supset .p\lor (r\lor q)}}
Dem.
[
Perm
q
,
r
p
,
q
]
⊢:
q
∨
r
.
⊃
.
r
∨
q
:
[
Sum
q
∨
r
,
r
∨
q
q
,
r
]
⊃
⊢:
p
∨
(
q
∨
r
)
.
⊃
.
p
∨
(
r
∨
q
)
{\displaystyle {\begin{array}{ll}\scriptstyle {\left[{\text{Perm}}{\frac {q,r}{p,q}}\right]\quad }&\scriptstyle {\vdash :q\lor r.\supset .r\lor q:}\\\scriptstyle {\left[{\text{Sum}}{\frac {q\lor r,r\lor q}{q,~~~r}}\right]\supset }&\scriptstyle {\vdash :p\lor (q\lor r).\supset .p\lor (r\lor q)}\end{array}}}
*2·31.
⊢:
p
∨
(
q
∨
r
)
.
⊃
.
(
p
∨
q
)
∨
r
{\displaystyle \scriptstyle {\vdash :p\lor (q\lor r).\supset .(p\lor q)\lor r}}
This proposition and *2·32 together constitute the associative law for logical addition of propositions. In the proof, the following abbreviation (constantly used hereafter) will be employed[ 1] : When we have a series of propositions of the form
a
⊃
b
{\displaystyle \scriptstyle {a\supset b}}
,
b
⊃
c
{\displaystyle \scriptstyle {b\supset c}}
,
c
⊃
d
{\displaystyle \scriptstyle {c\supset d}}
, all asserted, and "
a
⊃
d
{\displaystyle \scriptstyle {a\supset d}}
" is the proposition to be proved, the proof in full is as follows:
[
Syll
]
⊢:
.
a
⊃
b
.
⊃:
b
⊃
c
.
⊃
.
a
⊃
c
(
1
)
⊢:
a
.
⊃
.
b
(
2
)
[
(
1
)
.
(
2
)
.
∗
1
⋅
11
]
⊢:
b
⊃
c
.
⊃
.
a
⊃
c
(
3
)
⊢:
b
.
⊃
.
c
(
4
)
[
(
3
)
.
(
4
)
.
∗
1
⋅
11
]
⊢:
a
.
⊃
.
c
(
5
)
[
Syll
]
⊢:
.
a
⊃
c
.
⊃:
c
⊃
d
.
⊃
.
a
⊃
d
(
6
)
[
(
5
)
.
(
6
)
.
∗
1
⋅
11
]
⊢:
c
⊃
d
.
⊃
.
a
⊃
d
(
7
)
⊢:
c
.
⊃
.
d
(
8
)
[
(
7
)
.
(
8
)
.
∗
1
⋅
11
]
⊢:
a
.
⊃
.
d
{\displaystyle {\begin{array}{lll}\scriptstyle {[{\text{Syll}}]\quad }&\scriptstyle {\vdash :.a\supset b.\supset :b\supset c.\supset .a\supset c\qquad \qquad }&\scriptstyle {(1)}\\&\scriptstyle {\vdash :a.\supset .b}&\scriptstyle {(2)}\\\scriptstyle {[(1).(2).*1\cdot 11]}&\scriptstyle {\vdash :b\supset c.\supset .a\supset c}&\scriptstyle {(3)}\\&\scriptstyle {\vdash :b.\supset .c}&\scriptstyle {(4)}\\\scriptstyle {[(3).(4).*1\cdot 11]}&\scriptstyle {\vdash :a.\supset .c}&\scriptstyle {(5)}\\\scriptstyle {[{\text{Syll}}]}&\scriptstyle {\vdash :.a\supset c.\supset :c\supset d.\supset .a\supset d}&\scriptstyle {(6)}\\\scriptstyle {[(5).(6).*1\cdot 11]}&\scriptstyle {\vdash :c\supset d.\supset .a\supset d}&\scriptstyle {(7)}\\&\scriptstyle {\vdash :c.\supset .d}&\scriptstyle {(8)}\\\scriptstyle {[(7).(8).*1\cdot 11]}&\scriptstyle {\vdash :a.\supset .d}\end{array}}}
It is tedious to write out this process in full; we therefore write simply
⊢:
a
.
⊃
.
b
.
[
etc.
]
⊃
.
c
.
[
etc.
]
⊃
.
d
:⊃⊢
.
Prop,
{\displaystyle {\begin{aligned}\scriptstyle {\vdash :a.}&\scriptstyle {\supset .b.}\\\scriptstyle {[{\text{etc.}}]}&\scriptstyle {\supset .c.}\\\scriptstyle {[{\text{etc.}}]}&\scriptstyle {\supset .d:\supset \vdash .{\text{Prop,}}}\end{aligned}}}
where "
a
⊃
d
{\displaystyle \scriptstyle {a\supset d}}
" is the proposition to be proved. We indicate on the left by references in square brackets the propositions in virtue of which the successive implications hold. We put one dot (not two) after "
b
{\displaystyle \scriptstyle {b}}
," to show
↑ This abbreviation applies to the same type of cases as those concerned in the note to *2·15 , but is often more convenient than the abbreviation explained in that note.