Here is an English argument whose derivation exhibits all of the rules for negation:
|
Ann’s proposal wasn’t unfunded without Bill’s and Carol’s each being funded
Bill’s proposal was not funded Ann’s proposal was funded |
And here is the derivation:
| │¬ (¬ A ∧ ¬ (B ∧ C)) | 2 | |
| │¬ B | (7) | |
| ├─ | ||
| ││¬ A | (4) | |
| │├─ | ||
| ││││● | ||
| │││├─ | ||
| 4 QED | ││││¬ A | 3 |
| │││ | ||
| │││││B ∧ C | 6 | |
| ││││├─ | ||
| 6 Ext | │││││B | |
| 6 Ext | │││││C | |
| │││││● | ||
| ││││├─ | ||
| 7 Nc | │││││⊥ | 5 |
| │││├─ | ||
| 5 RAA | ││││¬ (B ∧ C) | 3 |
| ││├─ | ||
| 3 Cnj | │││¬ A ∧ ¬ (B ∧ C) | 2 |
| │├─ | ||
| 2 CR | ││⊥ | 1 |
| ├─ | ||
| 1 IP | │A |
One alternative approach would be to introduce ¬ (B ∧ C) as a lemma at the second stage using LFR.
In the absence of the rules of this section, the exercise 2d of 3.2.x required use of LFR. Here are two derivations for it that differ in the choice of the premise to be exploited by CR.
|
|
These derivations have the same number of stages as the answer in 3.2.xa for 2d, but their scope lines are nested one deeper. Each of the arguments completing the gaps set up by LFR in the earlier derivation appears in one of these; but we arrive at these arguments in a different way.
It is possible to dispense with Adj, too, and exploit both premises by CR. This leads to a derivation with two more stages and scope lines that are nested more deeply. What we get in return for that increased complexity is direction in how to complete the derivation. In effect, all the thinking required to identify appropriate lemmas is done on paper. The next subsection shows stage by stage how this derivation proceeds.