SECTION A ]
IMMEDIATE CONSEQUENCES
105
In the last line of this proof, "
(
1
)
.
(
2
)
.
∗
1
⋅
11
{\displaystyle \scriptstyle {(1).(2).*1\cdot 11}}
" means that we are inferring in accordance with *1·11 , having before us a proposition, namely
p
⊃
q
.
⊃:
q
⊃
r
.
⊃
.
p
⊃
r
{\displaystyle \scriptstyle {p\supset q.\supset :q\supset r.\supset .p\supset r}}
, which, by (1), is implied by
q
⊃
r
.
⊃:
p
⊃
q
.
⊃
.
p
⊃
r
{\displaystyle \scriptstyle {q\supset r.\supset :p\supset q.\supset .p\supset r}}
, which, by (2), is true. In general, in such cases, we shall omit the reference to *1·11.
The above two propositions will both be referred to as the "principle of the syllogism" (shortened to "Syll."), because, as will appear later, the syllogism in Barbara is derived from them.
*2·07.
⊢:
p
.
⊃
.
p
∨
p
[
∗
1
⋅
3
p
q
]
{\displaystyle \scriptstyle {\vdash :p.\supset .p\lor p\quad \left[*1\cdot 3{\frac {p}{q}}\right]}}
Here we put nothing beyond "
∗
1
⋅
3
p
q
{\displaystyle \scriptstyle {*1\cdot 3{\frac {p}{q}}}}
," because the proposition to be proved is what *1·3 becomes when
p
{\displaystyle \scriptstyle {p}}
is written in place of
q
{\displaystyle \scriptstyle {q}}
.
*2·08.
⊢
.
p
⊃
p
{\displaystyle \scriptstyle {\vdash .p\supset p}}
Dem.
[
∗
2
⋅
05
p
∨
p
,
p
q
,
r
]
⊢::
p
∨
p
.
⊃
.
p
:⊃:
.
p
.
⊃
.
p
∨
p
:⊃
.
p
⊃
p
(
1
)
[
Taut
]
⊢:
p
∨
p
.
⊃
.
p
(
2
)
[
(
1
)
.
(
2
)
.
∗
1
⋅
11
]
⊢:
.
p
.
⊃
.
p
∨
p
:⊃
.
p
⊃
p
(
3
)
[
2
⋅
07
]
⊢:
p
.
⊃
.
p
∨
p
(
4
)
[
(
3
)
.
(
4
)
.
∗
1
⋅
11
]
⊢
.
p
⊃
p
{\displaystyle {\begin{array}{lll}\scriptstyle {\left[*2\cdot 05{\frac {p\lor p,p}{q,~~r}}\right]\quad }&\scriptstyle {\vdash ::p\lor p.\supset .p:\supset :.p.\supset .p\lor p:\supset .p\supset p\qquad \qquad }&\scriptstyle {(1)}\\\scriptstyle {[{\text{Taut}}]\quad }&\scriptstyle {\vdash :p\lor p.\supset .p\qquad \qquad }&\scriptstyle {(2)}\\\scriptstyle {[(1).(2).*1\cdot 11]\quad }&\scriptstyle {\vdash :.p.\supset .p\lor p:\supset .p\supset p\qquad \qquad }&\scriptstyle {(3)}\\\scriptstyle {[2\cdot 07]\quad }&\scriptstyle {\vdash :p.\supset .p\lor p\qquad \qquad }&\scriptstyle {(4)}\\\scriptstyle {[(3).(4).*1\cdot 11]\quad }&\scriptstyle {\vdash .p\supset p\qquad \qquad }&\end{array}}}
2·1.
⊢
.
∼
p
∨
p
[
Id.
(
∗
1
⋅
01
)
]
{\displaystyle \scriptstyle {\vdash .\sim p\lor p\quad [{\text{Id.}}(*1\cdot 01)]}}
*2·11.
⊢
.
p
∨
∼
p
{\displaystyle \scriptstyle {\vdash .p\lor \sim p}}
Dem.
[
Perm
∼
p
,
p
p
,
q
]
⊢:∼
p
∨
p
.
⊃
.
p
∨
∼
p
(
1
)
[
(
1
)
.
∗
2
⋅
1.
∗
1
⋅
11
]
⊢
.
p
∨
∼
p
{\displaystyle {\begin{array}{lll}\scriptstyle {\left[{\text{Perm}}{\frac {\sim p,p}{p,~~q}}\right]\quad }&\scriptstyle {\vdash :\sim p\lor p.\supset .p\lor \sim p\qquad \qquad }&\scriptstyle {(1)}\\\scriptstyle {[(1).*2\cdot 1.*1\cdot 11]\quad }&\scriptstyle {\vdash .p\lor \sim p\qquad \qquad }&\end{array}}}
This is the law of excluded middle.
*2·12.
⊢
.
p
⊃∼
(
∼
p
)
{\displaystyle \scriptstyle {\vdash .p\supset \sim (\sim p)}}
Dem.
[
∗
2
⋅
11
∼
p
p
]
⊢
.
∼
p
∨
∼
(
∼
p
)
(
1
)
[
(
1
)
.
(
∗
1
⋅
01
)
]
⊢
.
p
⊃∼
(
∼
p
)
{\displaystyle {\begin{array}{lll}\scriptstyle {\left[*2\cdot 11{\frac {\sim p}{p}}\right]\quad }&\scriptstyle {\vdash .\sim p\lor \sim (\sim p)\qquad \qquad }&\scriptstyle {(1)}\\\scriptstyle {[(1).(*1\cdot 01)]\quad }&\scriptstyle {\vdash .p\supset \sim (\sim p)\qquad \qquad }&\end{array}}}