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 it will correspond to a particular way of growing chains of conclusions: always drawing conclusions by both left and right Ext from the end of one of them. The law for conjunction as a premise 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. This means that, when we use left and right extraction together, we can eliminate any further need to consider the conjunction we are exploiting. Because we always add both components of a conjunction we exploit, a derivation may contain conclusions that are never used later and would not appear in the corresponding proof tree.

Although we will apply left and right extraction together, we do not duplicate the shared segment of the two resulting chains, so the derivation rule Extraction 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 one 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 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 must continue to the left of the gap.

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 is already among the active resources of the gap, this component need not be added again, but there is nothing wrong with doing so. The number n of this 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 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 its 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 mark by a horizontal line. In English argumentation, words and phrases like therefore, hence, and it follows that indicate the same sorts of connections though in a less explicit way.

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 Conjunction 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 are introduced as premises from which the old one may be concluded while the resources added by Ext are added as conclusions drawn from the resource that is exploited; but, in both cases, the numbers mark a connection between premises and conclusions. The numbers here also serve, as do those for Ext, to show that an element of the derivation has been superceded by new additions. But, in the case of Cnj, this information is also provided in other ways: 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 shortly. But, when we are dealing with conjunction alone, it is possible to mimic the procedure used for tree-form proofs and 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, 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 phrase quod erat demonstrandum, which might be translated as what was to be proven. This Latin phrase 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, it is filled with the symbol ● (a black circle). 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.