2.2.2. Derivations

The tree-form proofs of the last section are probably the clearest way of presenting the structure of proofs; however, they are not very compact. This is in part because they are two-dimensional and in part because the premises and any conclusions reached from them by Ext may be repeated several times in the proof. In practice, we will use a more linear, though still somewhat two-dimensional, notation. We will gain compactness by writing premises and conclusions in a more-or-less vertical way and by minimizing the repetition of premises that are used draw a number of conclusions. But we also make other gains. The notation is designed to incorporate more directly the process of proof discovery presented in the last section by way of analysis trees and exploitation chains. And the notation will approximate some of the ways the structure of proofs is reflected in the essentially linear way argumentation is presented in language. Indeed, although we will not approach in this way, the notation for proofs could be thought of as a notation for analyzing the form of proofs presented in English that is in some respects analogous to our symbolic notation for analyzing the logical forms of sentences.

This machinery will be, as are tree-form proofs, much more than we need to settle questions of entailment involving only conjunction. But we will need more complex approaches eventually; and, because we have simpler ways of seeing that entailments hold in the case of conjunction, it will be easier to see how and why this method works if we develop it now.

The system to be developed here falls into a broad class often referred to as natural deduction systems because they replicate, to some extent, natural patterns of reasoning. Such systems were first set out in full in the 1930s by G. Gentzen and also by S. Jaskowski, but some of the key ideas can be found already in the Stoic philosopher Chrysippus (who lived in the 3rd century B. C.). The notation we will be using is an adaptation of notation introduced by F. B. Fitch but our approach to these systems will be influenced heavily by the semantic tableaux of E. Beth. (Their ideas are now about 50 years old.)

This system, which we will call a system of derivations, will employ a perspective on proofs that we adopted in the last section whenever we considered ways of restating claims of entailment. If we ask whether an entailment holds, we find ourselves faced with the task of reaching the conclusion from the premises (or showing that it cannot be reached). Let us think of the conclusion as our goal and of the premises as the resources we have available in trying to reach that goal. Until we reach the goal, it is separated from our resources by a gap that it is our aim to close.

We will approach the problem of closing this gap (or showing that it cannot be closed) step by step, at each step analyzing our goal (as in an analysis tree) or exploiting our resources (as in an exploitation chain). In making a step of either sort, we will restate our problem with different goals or resources; and we will say that, in restating it in this way, we are developing the derivation. The problem of closing a gap as seen from this perspective corresponds to the problem of finding exploitation chains to attach to all branches of an analysis tree, and the development of a derivation amounts to the process of growing analysis trees and exploitation chains in hopes of making this connection.

Although in the last section we attempted to connect exploitations chains to analysis trees only when both were fully grown, it would have been possible sometimes to make the connection at earlier points in their development; for the rule QED that is used to glue exploitation chains to analysis trees applies not only to unanalyzed components but to compounds as well. As we develop a derivation, we will, in effect, be watching the growth of analysis trees and exploitation chains looking for opportunities to connect them. We begin with a single gap between the premises and conclusion our initial question concerns. This gap can be closed immediately if the conclusion is among the premises. Otherwise we will analyze our goal (at first the original conclusion) or exploit our resources (at first the original premises). When we analyze a goal, we establish subgoals, intermediate conclusions from which the goal can be reached by Cnj. This divides the problem into subproblems, each focused on the gap between our resources and one of these new goals. As we exploit resources by Exp, we make new resources available to connect to our goals. If the goals and unexploited resources all end up as unanalyzed components, we have done as much as we can to prepare gaps to be closed and, if they cannot be closed at this point, we know that the initial argument is not valid.

A derivation will be written as a more or less vertical list of sentences marked up in various ways to indicate the structure of the corresponding tree-like proof. The subgoals that would be introduced by branching an analysis tree will be written one above the other, each preceded by space for further growth, and exploitation chains will be collapsed by superimposing any shared segments.

We begin in the state shown in Figure 2.2.2-1. The premises of the argument (if it has any) are written above a horizontal line, and the conclusion is written below a second line. The space in between the horizontal lines marks the gap and will be filled in with additional resources and new goals as the derivation develops. The vertical line at the left is a scope line and will serve us in a number of ways. First of all, new scope lines will be introduced as we analyze goals with a separate scope line serving to mark the portion of the derivation devoted to further analysis of each subgoal. This part of subderivation is where the subgoal is the conclusion we seek to establish, and it is in this sense the scope of the subgoal. As scope lines accumulate, they will be nested, some to the right of others, in a way that indicates the branching of an analysis tree. In later chapters, proofs will sometimes involve assumptions beyond the initial premises, and scope lines will then also serve to mark the portions of a proof in which these assumptions are being made. Later still, the scope lines will be labeled to indicate vocabulary that has a special role in a portion of a derivation.

At any stage in the development of a derivation, each gap will have certain active resources. These are resources available for use in the gap that have not already been exploited in developing it; they correspond, roughly, to the ends of exploitation chains at a given stage in their growth. Our aim will always be to see whether the goal of a gap is entailed by its active resources.