110
MATHEMATICAL LOGIC
[PART I
that it is
b
{\displaystyle \scriptstyle {b}}
, not "
a
⊃
b
{\displaystyle \scriptstyle {a\supset b}}
," that implies
c
{\displaystyle \scriptstyle {c}}
. But we put two dots after
d
{\displaystyle \scriptstyle {d}}
, to show that now the whole proposition "
a
⊃
d
{\displaystyle \scriptstyle {a\supset d}}
" is concerned. If "
a
⊃
d
{\displaystyle \scriptstyle {a\supset d}}
" is not the proposition to be proved, but is to be used subsequently in the proof, we put
⊢:
a
.
⊃
.
b
.
[
etc.
]
⊃
.
c
.
[
etc.
]
⊃
.
d
(1),
{\displaystyle {\begin{array}{ll}\scriptstyle {\vdash :a.}&\scriptstyle {\supset .b.}\\\scriptstyle {[{\text{etc.}}]}&\scriptstyle {\supset .c.}\\\scriptstyle {[{\text{etc.}}]}&\scriptstyle {\supset .d\qquad \qquad \qquad \qquad \qquad {\text{(1),}}}\end{array}}}
and then "
(
1
)
{\displaystyle \scriptstyle {(1)}}
" means "
a
⊃
d
{\displaystyle \scriptstyle {a\supset d}}
." The proof of *2·31 is as follows:
Dem.
[
∗
2
⋅
3
]
⊢:
p
∨
(
q
∨
r
)
.
⊃
.
p
∨
(
r
∨
q
)
.
[
Assoc
r
,
q
q
,
r
]
⊃
.
r
∨
(
p
∨
q
)
.
[
Perm
r
,
p
∨
q
p
,
q
]
⊃
.
(
p
∨
q
)
∨
r
:⊃⊢
.
Prop
{\displaystyle {\begin{array}{ll}\scriptstyle {[*2\cdot 3]\vdash :p\lor (q\lor r).}&\scriptstyle {\supset .p\lor (r\lor q).}\\\scriptstyle {\left[{\text{Assoc}}{\frac {r,q}{q,r}}\right]\quad }&\scriptstyle {\supset .r\lor (p\lor q).}\\\scriptstyle {[{\text{Perm}}{\frac {r,p\lor q}{p,~~q}}]\quad }&\scriptstyle {\supset .(p\lor q)\lor r:\supset \vdash .{\text{Prop}}}\end{array}}}
*2·32.
⊢:
(
p
∨
q
)
∨
r
.
⊃
.
p
∨
(
q
∨
r
)
{\displaystyle \scriptstyle {\vdash :(p\lor q)\lor r.\supset .p\lor (q\lor r)}}
Dem.
[
Perm
p
∨
q
,
r
p
,
q
]
⊢:
(
p
∨
q
)
∨
r
.
⊃
.
r
∨
(
p
∨
q
)
[
Assoc
r
,
p
,
q
p
,
q
,
r
]
⊃
.
p
∨
(
r
∨
q
)
[
∗
2
⋅
3
]
⊃
.
p
∨
(
q
∨
r
)
:⊃⊢
.
Prop
{\displaystyle {\begin{array}{ll}\scriptstyle {\left[{\text{Perm}}{\frac {p\lor q,r}{p,~q}}\right]\vdash :(p\lor q)\lor r.}&\scriptstyle {\supset .r\lor (p\lor q)}\\\scriptstyle {\left[{\text{Assoc}}{\frac {r,p,q}{p,q,r}}\right]}&\scriptstyle {\supset .p\lor (r\lor q)}\\\scriptstyle {[*2\cdot 3]}&\scriptstyle {\supset .p\lor (q\lor r):\supset \vdash .{\text{Prop}}}\end{array}}}
*2·33.
p
∨
q
∨
r
.
=
.
(
p
∨
q
)
∨
r
Df
{\displaystyle \scriptstyle {p\lor q\lor r.=.(p\lor q)\lor r\quad {\text{Df}}}}
This definition serves only for the avoidance of brackets.
*2·36.
⊢:
.
q
⊃
r
.
⊃:
p
∨
q
.
⊃
.
r
∨
p
{\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :p\lor q.\supset .r\lor p}}
Dem.
[
Perm
]
⊢:
p
∨
r
.
⊃
.
r
∨
p
:
[
Syll
p
∨
q
,
p
∨
r
,
r
∨
p
p
,
q
,
r
]
⊃
⊢:
.
p
∨
q
.
⊃
.
p
∨
r
:⊃:
p
∨
q
.
⊃
.
r
∨
p
(
1
)
[
Sum
]
⊢:
.
q
⊃
r
.
⊃:
p
∨
q
.
⊃
.
p
∨
r
(
2
)
⊢
.
(
1
)
.
(
2
)
.
S
y
l
l
.
⊃⊢
.
Prop
{\displaystyle {\begin{array}{lll}\scriptstyle {[{\text{Perm}}]}&\scriptstyle {\vdash :p\lor r.\supset .r\lor p:}\\\scriptstyle {\left[{\text{Syll}}{\frac {p\lor q,p\lor r,r\lor p}{p,~~q,~~r}}\right]\supset }&\scriptstyle {\vdash :.p\lor q.\supset .p\lor r:\supset :p\lor q.\supset .r\lor p\quad }&\scriptstyle {(1)}\\\scriptstyle {[{\text{Sum}}]}&\scriptstyle {\vdash :.q\supset r.\supset :p\lor q.\supset .p\lor r}&\scriptstyle {(2)}\\\scriptstyle {\vdash .(1).(2).Syll.\supset \vdash .{\text{Prop}}}\end{array}}}
*2·37.
⊢:
.
q
⊃
r
.
⊃:
q
∨
p
.
⊃
.
p
∨
r
{\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :q\lor p.\supset .p\lor r}}
[
Syll
.
Perm
.
Sum
]
{\displaystyle \scriptstyle {[{\text{Syll}}.{\text{Perm}}.{\text{Sum}}]}}
*2·38.
⊢:
.
q
⊃
r
.
⊃:
q
∨
p
.
⊃
.
r
∨
p
{\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :q\lor p.\supset .r\lor p}}
[
Syll
.
Perm
.
Sum
]
{\displaystyle \scriptstyle {[{\text{Syll}}.{\text{Perm}}.{\text{Sum}}]}}
The proofs of *2·37·38 are exactly analogous to that of *2·36. (We use "*2·37·38" as an abbreviation for "*2·37 and *2·38." Such abbreviations will be used throughout.)