Subderivations can be nested. For an example, we provide a derivation for the argument
∴
We begin with the premises and then assume the antecedent of the conclusion.
Note. Each time we begin a new subderivation and enter a temporary assumption, there is a specific formula we are hoping to derive when it comes time to end the derivation and discharge the assumption. To make things easier to follow, we will add this formula to the annotation of the assumption. That formula will not officially be part of the annotation and does not affect the correctness of the derivation. Instead, it will serve as an informal reminder to ourselves noting where we are going.
1.
Premise
2.
Premise
3.
Premise
4.
Assumption
This starts a subderivation to derive the argument's conclusion. Now we will try a Disjunction Elimination (DE) to derive its consequent:
This will require the showing two conditionals we need for the antecedent lines of a DE, namely:
and
We begin with the first of these conditionals.
5.
Assumption
6.
Assumption
This subderivation is easily finished.
7.
5, 6 KI
8.
1, 7 CE
9.
2 KE
Now we are ready to discharge the two assumptions at Lines 5 and 6.
10.
6–9 NI
11.
5–10 CI
Now it's time for the second conditional needed for our DE planned back at Line 4. We begin.
12.
Assumption
13.
Assumption
14.
2 KE
15.
3, 14 CE
Note that we have a contradiction between Lines 12 and 15. But line 12 is in the wrong place. We need it in the same subderivation as Line 15. A silly trick at Lines 16 and 17 below will accomplish that. Then the assumptions at Lines 12 and 13 can be discharged.
16.
12, 12 KI
17.
16 KE
18.
13–17 NI
19.
12–18 CI
Finally, with Lines 4, 11, and 19, we can perform the DE we've been wanting since Line 4.
20.
4, 11, 19 DE
Now to finish the derivation by discharging the assumption at Line 4.
![{\displaystyle [\mathrm {P} \lor \mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aa44596d60b688c05bbdbe0bc7247ed056fb546a)
![{\displaystyle [\mathrm {P} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/94b1bf4e357c16d14c5edd2c38d2d82c0bcf02ac)
![{\displaystyle [\lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8b390160716315f88a8ad089d9a9d61428354ee)
![{\displaystyle [\mathrm {Q} \rightarrow \lnot \mathrm {R} ]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e985539e01255392f5c1c6fe670de638714a63f8)
