2.2.3. Derivations

Both conclusion trees and argument trees spread out in two dimensions. 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. These will grow left to right like argument trees; and, indeed, this notation consists most essentially of argument trees that have been squashed from branch tips to root.

Compactness is not all we will gain with this notation. It 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 now go back about 60 years.)

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 lies on the other side of a gap that it is our aim to close.

We begin in the state shown in Figure 2.2.3-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. Although conclusion trees will be only in the background of these derivations, the process of filling a gap from both ends to the middle that was displayed in Figure 2.2.2-2 is closely related to this sort of development.

This 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 ψ individually, for we will then set each of φ and ψ as a preliminary goal and each will have a gap before it. This development of our initial problem by restating it and perhaps dividing it into subproblems will be expressed in a sort of tree structure just as it is in argument trees. 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.3-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. These resources can be used to form the premises of an argument, using the gap’s goal as its conclusion. We will call this argument the proximate argument to distinguish it from the ultimate argument for which the derivation is being constructed. Our aim in a developing a gap will always be to see whether the goal of the gap is entailed by its active resources, whether its proximate argument is valid. And this means that the situation depicted in Figure 2.2.3-1, which is explicit at the beginning of the derivation for the case of the ultimate argument, will be replicated, although less explicitly, for proximate arguments throughout the development of a derivation. This is the way derivations are associated with argument trees: the proximate arguments of the gaps of a derivation form an argument tree, and the development of the derivation is really the development of this tree. The argument tree and conclusion tree associated with a derivation may not be immediately apparent, but their presence will be felt in the bookkeeping required by the system of scope lines and stage numbers. This bookkeeping is the price paid for using less space and less repetition in writing.