Disjunctions in Derivations
edit
Disjunctions in derivations are, as the current inference rules stand, difficult to deal with. Using an already derived disjunction by applying Disjunction Elimination (DE) is not too bad, but there is an easier to use alternative. Deriving a disjunction in the first place is more difficult. Our Disjunction Introduction (DI) rule turns out to be a rather anemic tool for this task. In this module, we introduce derived rules which provide alternative methods for dealing with disjunctions in derivations.
Using already derived disjunctions
edit
Modus Tollendo Ponens
edit
We start with a new (to be) derived rule of inference. This will provide a useful alternative to Disjunction Elimination (DE).
Modus Tollendo Ponens, Form I (MTP)
(
φ
∨
ψ
)
{\displaystyle (\varphi \lor \psi )\,\!}
¬
φ
_
{\displaystyle {\underline {\lnot \varphi \quad \quad }}\,\!}
ψ
{\displaystyle \psi \,\!}
Modus Tollendo Ponens, Form II (MTP)
(
φ
∨
ψ
)
{\displaystyle (\varphi \lor \psi )\,\!}
¬
ψ
_
{\displaystyle {\underline {\lnot \psi \quad \quad }}\,\!}
φ
{\displaystyle \varphi \,\!}
Modus Tollendo Ponens is sometimes known as Disjunctive Syllogism and occasionally as the Rule of the Dog.
Supporting theorems
edit
This new rule requires the following two supporting theorems.
T
16.
(
P
∨
Q
)
∧
¬
P
→
Q
{\displaystyle \mathbf {T16.} \quad (\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!}
1.
(
P
∨
Q
)
∧
¬
P
{\displaystyle (\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \,\!}
Assumption
[
(
P
∨
Q
)
∧
¬
P
→
Q
]
{\displaystyle [(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} ]\,\!}
2.
P
∨
Q
{\displaystyle \mathrm {P} \lor \mathrm {Q} \,\!}
1 KE
3.
¬
P
{\displaystyle \lnot \mathrm {P} \,\!}
1 KE
4.
P
→
Q
{\displaystyle \mathrm {P} \rightarrow \mathrm {Q} \,\!}
3 CAdd
5.
Q
→
Q
{\displaystyle \mathrm {Q} \rightarrow \mathrm {Q} \,\!}
T1 [P /Q ]
6.
Q
{\displaystyle \mathrm {Q} \,\!}
2, 4, 5 DE
7.
(
P
∨
Q
)
∧
¬
P
→
Q
{\displaystyle (\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!}
1–6 CI
T
17.
(
P
∨
Q
)
∧
¬
Q
→
P
{\displaystyle \mathbf {T17.} \quad (\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} \,\!}
1.
(
P
∨
Q
)
∧
¬
Q
{\displaystyle (\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \,\!}
Assumption
[
(
P
∨
Q
)
∧
¬
Q
→
P
]
{\displaystyle [(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} ]\,\!}
2.
P
∨
Q
{\displaystyle \mathrm {P} \lor \mathrm {Q} \,\!}
1 KE
3.
¬
Q
{\displaystyle \lnot \mathrm {Q} \,\!}
1 KE
4.
Q
→
P
{\displaystyle \mathrm {Q} \rightarrow \mathrm {P} \,\!}
3 CAdd
5.
P
→
P
{\displaystyle \mathrm {P} \rightarrow \mathrm {P} \,\!}
T1
6.
P
{\displaystyle \mathrm {P} \,\!}
2, 4, 5 DE
7.
(
P
∨
Q
)
∧
¬
Q
→
P
{\displaystyle (\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} \,\!}
1–6 CI
Example derivation
edit
For an example using MTP, we redo the example derivation from Constructing a Complex Derivation .
P
∧
R
→
T
,
S
∧
¬
T
,
S
→
¬
Q
{\displaystyle \mathrm {P} \land \mathrm {R} \rightarrow \mathrm {T} ,\ \ \mathrm {S} \land \lnot \mathrm {T} ,\ \ \mathrm {S} \rightarrow \lnot \mathrm {Q} \,\!}
∴
P
∨
Q
→
¬
R
{\displaystyle \mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} \,\!}
1.
P
∧
R
→
T
{\displaystyle \mathrm {P} \land \mathrm {R} \rightarrow \mathrm {T} \,\!}
Premise
2.
S
∧
¬
T
{\displaystyle \mathrm {S} \land \lnot \mathrm {T} \,\!}
Premise
3.
S
→
¬
Q
{\displaystyle \mathrm {S} \rightarrow \lnot \mathrm {Q} \,\!}
Premise
4.
P
∨
Q
{\displaystyle \mathrm {P} \lor \mathrm {Q} \,\!}
Assumption
[
P
∨
Q
→
¬
R
]
{\displaystyle [\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!}
5.
R
{\displaystyle \mathrm {R} \,\!}
Assumption
[
¬
R
]
{\displaystyle [\lnot \mathrm {R} ]\,\!}
6.
S
{\displaystyle \mathrm {S} \,\!}
2 KE
7.
¬
Q
{\displaystyle \lnot \mathrm {Q} \,\!}
3, 6 CE
8.
P
{\displaystyle \mathrm {P} \,\!}
4, 7 MTP
9.
P
∧
R
{\displaystyle \mathrm {P} \land \mathrm {R} \,\!}
5, 8 KI
10.
T
{\displaystyle \mathrm {T} \,\!}
1, 9 CE
11.
¬
T
{\displaystyle \lnot \mathrm {T} \,\!}
2 KE
12.
¬
R
{\displaystyle \lnot \mathrm {R} \,\!}
5–11 NI
13.
P
∨
Q
→
¬
R
{\displaystyle \mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} \,\!}
4–12 CI
Deriving disjunctions
edit
Conditional Disjunction
edit
The next derived rule significantly reduces the labor of deriving disjunctions, thus providing a useful alternative to Disjunction Introduction (DI).
Conditional Disjunction (CDJ)
(
¬
φ
→
ψ
)
_
{\displaystyle {\underline {(\lnot \varphi \rightarrow \psi )}}\,\!}
(
φ
∨
ψ
)
{\displaystyle (\varphi \lor \psi )\,\!}
Supporting theorem
edit
T
18.
(
¬
P
→
Q
)
→
P
∨
Q
{\displaystyle \mathbf {T18.} \quad (\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} \,\!}
1.
¬
P
→
Q
{\displaystyle \lnot \mathrm {P} \rightarrow \mathrm {Q} \,\!}
Assumption
[
(
¬
P
→
Q
)
→
P
∨
Q
]
{\displaystyle [(\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} ]\,\!}
2.
¬
(
P
∨
Q
)
{\displaystyle \lnot (\mathrm {P} \lor \mathrm {Q} )\,\!}
Assumption
[
P
∨
Q
]
{\displaystyle [\mathrm {P} \lor \mathrm {Q} ]\,\!}
3.
P
{\displaystyle \mathrm {P} \,\!}
Assumption
[
¬
P
]
{\displaystyle [\lnot \mathrm {P} ]\,\!}
4.
P
∨
Q
{\displaystyle \mathrm {P} \lor \mathrm {Q} \,\!}
3 DI
5.
¬
(
P
∨
Q
)
{\displaystyle \lnot (\mathrm {P} \lor \mathrm {Q} )\,\!}
2 R
6.
¬
P
{\displaystyle \lnot \mathrm {P} \,\!}
3–5 NI
7.
Q
{\displaystyle \mathrm {Q} \,\!}
1, 6 CE
8.
P
∨
Q
{\displaystyle \mathrm {P} \lor \mathrm {Q} \,\!}
7 DI
9.
P
∨
Q
{\displaystyle \mathrm {P} \lor \mathrm {Q} \,\!}
2–8 NI
10.
(
¬
P
→
Q
)
→
P
∨
Q
{\displaystyle (\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} \,\!}
1–9 CI
Example derivation
edit
This derivation will make use of T12 (introduced at Derived Inference Rules ) even though its proof was left to the reader as an exercise. The correctness the following derivation, particularly Line 2, assumes that you have indeed proved T12 .
∴
(
P
→
Q
)
∨
(
Q
→
R
)
{\displaystyle (\mathrm {P} \rightarrow \mathrm {Q} )\lor (\mathrm {Q} \rightarrow \mathrm {R} )\,\!}
1.
¬
(
P
→
Q
)
{\displaystyle \lnot (\mathrm {P} \rightarrow \mathrm {Q} )\,\!}
Assumption
[
¬
(
P
→
Q
)
→
(
Q
→
R
)
]
{\displaystyle [\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow (\mathrm {Q} \rightarrow \mathrm {R} )]\,\!}
2.
¬
(
P
→
Q
)
→
P
∧
¬
Q
{\displaystyle \lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \land \lnot \mathrm {Q} \,\!}
T12
3.
P
∧
¬
Q
{\displaystyle \mathrm {P} \land \lnot \mathrm {Q} \,\!}
1, 2 CE
4.
¬
Q
{\displaystyle \lnot \mathrm {Q} \,\!}
3 KE
5.
Q
→
R
{\displaystyle \mathrm {Q} \rightarrow \mathrm {R} \,\!}
4 CAdd
7.
¬
(
P
→
Q
)
→
(
Q
→
R
)
{\displaystyle \lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow (\mathrm {Q} \rightarrow \mathrm {R} )\,\!}
1–6 CI
8.
(
P
→
Q
)
∨
(
Q
→
R
)
{\displaystyle (\mathrm {P} \rightarrow \mathrm {Q} )\lor (\mathrm {Q} \rightarrow \mathrm {R} )\,\!}
7 CDJ
![{\displaystyle [(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {P} \rightarrow \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ce2fd880e79bd95061a9001884c5f98b39d25c94)
![{\displaystyle [(\mathrm {P} \lor \mathrm {Q} )\land \lnot \mathrm {Q} \rightarrow \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/017310eff4f2d7cae3bd6dd40e51e5acc578175e)
![{\displaystyle [\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aa44596d60b688c05bbdbe0bc7247ed056fb546a)
![{\displaystyle [\lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8b390160716315f88a8ad089d9a9d61428354ee)
![{\displaystyle [(\lnot \mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {P} \lor \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d274e3f04d76311583944ef8236ff241af80cfab)
![{\displaystyle [\mathrm {P} \lor \mathrm {Q} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d908c75773c25f4ce62e273bd9b6b7abe190692f)
![{\displaystyle [\lnot \mathrm {P} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ebecf005a1793b292d92ddec0a677c0612909c89)
![{\displaystyle [\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow (\mathrm {Q} \rightarrow \mathrm {R} )]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4f17aa6df957ee3265b637942af874d9ab1c05c8)
