3.3.3. More examples

Here is an English argument whose derivation exhibits all of the rules for negation:

And here is the derivation:

The rules of this section are used at the first two stages, and the rules of 3.2 are in the course of reaching the goal introduced by CR. One alternative approach would be to introduce ¬ (B ∧ C) as a lemma at the second stage using LFR. Combined with a use of Adj to add ¬ A ∧ ¬ (B ∧ C) as a resource, it would produce a simpler derivation but one that requires foresight to discover.

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 the argument of that exercise which use CR instead but differ in the choice of the premise to be exploited by this rule.

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 derivations, but we arrive at these arguments in a different way.

It is possible to dispense with Adj in the derivations above 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. We will look at this third approach to the example in 3.5, where we consider how the rules guide the search for derivations.