2.2.3. Rules for derivations

One way of developing a gap is to restate our problem so that one of its resources can be dropped from consideration, perhaps adding others of equivalent power but simpler form. We will call this process exploitation, and one example is provided by the way we implement the law for conjunction as a premise. That principle tells us that anything we can conclude from premises that include a conjunction can still be concluded if we replace the conjunction by its two components. In derivations, we will apply this idea by adding, as further resources, both of the conclusions that can reached from a conjunction by Ext. By adding both conclusions, we eliminate any further need to consider the conjunction we are exploiting; but, since both conclusions may not be needed to reach our ultimate goal, a derivation may contain conclusions that are never used later.

The derivation rule Extraction thus takes the form shown in Figure 2.2.3-1.

On the left, the gap is shown nested inside scope lines (two are shown but there may be just one or more than two). A conjunction is displayed at the top to show that it is among resources available for use in this gap. It is shown to the right of one of the scope lines running to the left of the gap but not to the right of the other. The requirement this illustrates is that a resource being exploited need not be inside all the scope lines to the left of the gap but cannot be inside any extra ones; that is, all lines to the left of the resource being exploited must continue to the left of the gap it is exploited in.

The right side of the figure illustrates the results of exploiting the conjunction. When we exploit it, we add its components as new resources at the top of the gap. If either component of the conjunction should happen to be already among the active resources of the gap, it would not be necessary to add this component again; but there is nothing wrong with doing so, and examples in the text will generally add it. (Although this practice may make the derivation slightly less compact, it makes it possible to focus solely on the parts of the derivation that are immediately relevant to the rule—i.e., the ones displayed in the diagram above.)

The number n of the new stage in the development of the derivation is written to the right of the conjunction to show that it has been exploited at this stage, and the stage number is also shown, along with the label Ext, to the left of each of the two lines that are added. Once the conjunction has been exploited, it is no longer an active resource for this gap though it could be active in other gaps (we will see later how to tell). The numbers in a derivation thus record the order of the development and also provide a way of telling when and where resources are exploited. These numbers are also one of the devices derivations use to encode the structure of tree-form proofs: they mark the relation between premises and conclusion that tree-form proofs marked the horizontal lines between premises and conclusions. In English argumentation, words and phrases like therefore, hence, and it follows that indicate the same sorts of connections in a less explicit way.

Exploiting resources like this is one way to narrow a gap. Another way to narrow a gap is to restate the problem it represents so that the goal we seek to reach is replaced by one or more simpler goals. We will call this process goal planning. The law for conjunction as a conclusion tells us how we may plan for a goal that is a conjunction. Such a goal is entailed by our active resources if and only if each of its components is entailed. So the project of reaching a conjunction φ ∧ ψ from given resources comes to the same thing as completing two projects—namely, reaching each of the components φ and ψ from those same resources. This sort of goal planning thus uses Cnj and takes the form shown in Figure 2.2.3-2.

On the left, no assumptions are made about the resources, but the goal is shown as a conjunction. On the right, we have introduced two new gaps, each with one of the conjunction’s components as its goal. The two new goals bring with them two scope lines and are marked off by horizontal lines (as was the initial conclusion) to show that they represent the new material that led to the use of new scope lines. At the right of each of the new goals is a number showing the stage at which it was added. The same number appears to the left of the goal along with the label Cnj.

While in the case of Ext, numbers appeared at the left of the resources that were added and at the right of the resource being exploited, numbers here appear on the right of the new goals and at the left of the old one. This is because the new goals added by Cnj are introduced as premises from which the old goal may be concluded while the resources added by Ext are added as conclusions drawn from the resource that is exploited. Still, in both cases the numbers mark a connection between premises and conclusions. The numbers also show for both rules how an element of the derivation has been superceded by new additions. But, in the case of Cnj, this information is also provided by the added gaps: a gap will always have exactly one goal, and that goal will appear immediately below it.

The new gaps introduced in planning for a conjunction initially have the same active resources as the original gap. As resources are exploited in narrowing one of the gaps, these resources will become inactive for that gap; but they will remain active for the other gap until they are exploited there. When a derivation contains more than one gap, the question of where resources are active becomes important, and something will be said about it before too long. But, when we are dealing with conjunction alone, it is possible to exploit the initial resources completely before we plan for goals. As a result, a general discussion of active and inactive resources can be postponed until we have considered an actual example of a derivation.

What we cannot postpone is an account of how a gap may be closed. If the goal of a gap appears also among its resources, the law for premises tells us that the goal is entailed by these resources. That means we have succeeded in making a connection between our resources and that goal, and the gap may be closed. The rule we use to do this is shown in Figure 2.2.3-3 below.

The label for this rule abbreviates the Latin quod erat demonstrandum (which might be translated as what was to be proven), a phrase that is traditionally used when a planned conclusion is reached.

The stage number appears to the left of the goal (along with the label) since the goal is the conclusion, and it appears to the right of the resource since the resource is the premise. The latter number is enclosed in parentheses to indicate that the premise is not here being exploited. Since the gap is closed, the question whether a resource is active or not becomes moot; but this sort of notation will be used later in other cases where resources are used without being replaced by simpler resources of equivalent content, and QED shares with these rules the feature that the resources to which it is applied do not need to be active. To make it easy to see that the gap is now closed, we put the symbol ● (a filled circle) in it. This is really not part of the derivation itself and is not given a stage number; it instead functions like stage numbers to indicate the organization of a derivation. Think of an analogy with written language: the symbol ● marks the end of a series of stages in the way a period marks the end of a series of words.