2.2.1. Proofs as trees

Our study of entailments involving conjunction will rest on the principles discussed in 2.1.1. These are shown below, in symbolic form on the left and in English on the right:

φ ∧ ψ ⊨ φ	both φ and ψ ⊨ φ
φ ∧ ψ ⊨ ψ	both φ and ψ ⊨ ψ
φ, ψ ⊨ φ ∧ ψ	φ, ψ ⊨ both φ and ψ.

We will refer to the first two of these patterns as extraction (left and right extraction to distinguish them) and to the third simply as conjunction. To establish particular cases of entailment, we will want to put together instances of these general patterns and, eventually, instances of other patterns, too. We will look at three different sorts of notation for doing this. It is the third, to be introduced in the next subsection, that we will employ in the end; but two others, which we will consider in the this subsection are useful for understanding the one we will actually use.

What may be the most direct notation for combining principles of entailment employs something like the two-dimensional form we have used for arguments, with the conclusion below the premises and marked off from them by a horizontal line. In order to make the premises of a multi-premised argument available to serve as conclusions of further argument, we will spread them out horizontally. In this style of notation, the basic patterns for conjunction take the following forms (where abbreviations of their names are used as labels):

φ ∧ ψ Ext φ

φ ∧ ψ Ext ψ

φ ψ Cnj φ ∧ ψ

To these we will add the one way of drawing conclusions available for all sentences:

While this adds no new conclusion, it will play a role in joining compound arguments that were constructed separately. The label for this rule reflects that role. It 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.

Arguments exhibiting these patterns can be linked by treating the premises of one argument as conclusions of other arguments. For example, the following shows that (A ∧ B) ∧ C is a valid conclusion from the two premises A and B ∧ C:

The ability to put entailments together in this way rests on the general laws of entailment discussed in 1.4.7. The law for premises enables us to begin; it shows that the premises A and B ∧ C entail the tips of the branches of this conclusion tree. Repeated uses of the chain law then enable us to add conclusions drawn using the principles for conjunction, and we work our way down the tree showing that the original set of premises entails each intermediate conclusion and, eventually, (A ∧ B) ∧ C. For example, just before the end, we know that our original premises entail each of the premises of the final conclusion—i.e., that A, B ∧ C ⊨ A ∧ B and A, B ∧ C ⊨ C. The chain law then enables us to combine these entailments with the fact that A ∧ B, C ⊨ (A ∧ B) ∧ C (a case of Conjunction) to show that A, B ∧ C ⊨ (A ∧ B) ∧ C.

The simplicity of these conclusion trees makes them useful for studying the general properties of proofs; however, we will employ a somewhat different way of representing proofs. One reason is that conclusion tree do not provide much support for discovering proofs. There is a small modification can help in that respect and that will lead us in the direction of the representation we will use. If we employ QED in the midst of a tree, we can distinguish separate components. That’s done here in the following proof showing that A ∧ (B ∧ C) ⊨ (A ∧ B) ∧ C:

Here we have three conclusion trees (mere unbranched saplings) drawing conclusions from the initial premise by Ext

A ∧ (B ∧ C) Ext A

A ∧ (B ∧ C) Ext B ∧ C Ext B

A ∧ (B ∧ C) Ext B ∧ C Ext C

glued to the tips of a tree deriving the desired conclusion by use of Cnj

Notice that the conclusions of the trees using Ext are all unanalyzed sentences, as are the premises of the tree using Cnj.

The net effect is that the premises simplify as you move down one of trees of using Ext from tip to root while there is simplification in the tree using Cnj when you move up from root to tip. Assuming that this can always be managed, it suggests a systematic way of finding a conclusion tree for given premises and conclusion: derive simpler premises from the initial ones using Ext and plan to get the final conclusion from simpler ones using Cnj.

That we can always construct a conclusion tree in this way follows from the two principles below. Although they are related to the validity of Ext and Cnj, they take a different form from principles stating the validity of particular patterns of argument. Instead they describe general conditions under which any arguments involving conjunction are valid.

These principles can be seen to hold by the comparing the sort of possible worlds each side of the if and only if rules out. To separate the premises of Γ, φ ∧ ψ / χ from its conclusion, we would need to do exactly what we’d need to do to separate the premises of Γ, φ, ψ / χ from its conclusion. And to separate the premises of Γ / φ ∧ ψ from its conclusion, we’d need to do exactly what we’d need to do the show the right side of the second law false—that is, separate premises from conclusion for at least one of Γ / φ and Γ / ψ.

The if parts of these principles reflect the validity of arguments of the forms Ext and Cnj, respectively, together with the chain law. For example, the if part of the first says that any valid conclusion from φ and ψ, perhaps along with other premises Γ, will follow from φ ∧ ψ along with those other premises, so we are not going astray as we move down a tree of premises. The only if parts tell us that the validity of the arguments on their left sides can always be established in the way licensed by the if part. For example, the only if part of the second tells us that, if a conjunction is a valid conclusion, then the premises needed to reach it by Cnj are bound to be valid conclusions also; so it should be possible to establish what we need to in order to apply Cnj. In sum, these two principles together show that the sort of mixed tree of premises and conclusions shown above will always suffice in constructing a proof.