2.2.2. Derivations

Both ways of writing proofs that we considered in the last section involved trees that spread horizontally. The more compact notation that we will actually use will be more linear, though still somewhat two-dimensional. We will gain compactness by listing 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. We will still need a tree structure to keep track of the premises relevant any given point, but this will involve rather stunted trees that grow horizontally from left to right.

Compactness is not all we will gain with this notation. It is designed to incorporate more directly the process of proof discovery, and it will approximate the ways proofs are normally stated in language. Indeed, although we will not emphasize this aspect of it, 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.

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 BCE). 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 a little over 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 begin in the state shown in Figure 2.2.2-1, with a single gap between the premises and conclusion the argument whose validity we are trying to establish.

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 on the left will be discussed later.)

We will approach the problem of closing the initial gap (or showing that it cannot be closed) step by step. At each step, either we will plan the way a goal may be reached or we will exploit resources, usually by drawing one or more conclusions from them. In making a step of either sort, we will restate our problem with different goals or resources, and we will say that, by this restatement, we are developing the derivation. When it is seen from this perspective, the problem of closing a gap is a problem of connecting available premises with desired conclusions. In developing a derivation, we work forward from premises and backward from conclusions in hopes of making this connection.

Either process may lead us to divide a gap in two. In the case of conjunction, this will happen when we plan to reach a goal φ ∧ ψ by first concluding φ and ψ separately, for we will then set φ and ψ as separate preliminary goals and there will be a gap before each of them. This development of our initial problem by restating it and perhaps dividing it into subproblems will be expressed in a sort of tree structure. However, a derivation will be written as a more or less vertical list of sentences. The subgoals that we plan to reach in order to go on to a further goal will be written one above the other, each preceded by space for further growth, and conclusions we reach by exploiting resources will be written in at the top of a gap. In order to indicate the tree structure of problems and subproblems within this vertical list of sentences, we will need to mark up the derivation in various ways.

We will employ two main devices for doing this. One is the numbering of stages and sentences added at those stages. The other device is a system of vertical lines like the line at the left in Figure 2.2.2-1. These lines will be called scope lines, and they 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 each subgoal. The scope line will indicate the portion of derivation where a given subgoal is the goal we are aiming at, and it is in this sense that the scope line marks scope of the subgoal. As scope lines accumulate, they will be nested, some to the right of others, in a way that indicates the tree structure of the proofs. 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 operative—that is, they will serve to mark the scope of assumptions as well as goals. Later still, the scope lines will be labeled to indicate vocabulary that has a special role in the portion of a derivation marked by the scope line.

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 to the premises appearing to the left of a given turnstile in the sequent proofs discussed in the last section. Our aim in a developing a gap will thus always be to see whether the goal of the gap is entailed by its active resources. And this means that the situation depicted in Figure 2.2.2-1, which is explicit at the beginning of the derivation, will be replicated, although less explicitly, throughout the development of a derivation.