3.3.3. More examples

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

And here is the derivation:

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 the same argument that 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; 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. We look at this third approach in 3.5, where we will look more closely at the way rules can guide the development of a derivation.