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:

We will refer to the first two of these patterns as extraction (left and right extraction when we wish to distinguish them) and to the third simply as conjunction. To establish particular cases of entailment, we will want to link together special cases of these general patterns and, eventually, of other patterns, too.

One notation for doing that 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):

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 the principles for conjunction 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 tree-like proof. Repeated uses of the chain law then enable 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.

These tree-form proofs are less helpful in the case of other connectives; and, in 2.3, we will look at a different way of arguing in the case of conjunction that is better suited to other logical forms. We can make one step in that direction now by looking at some basic principles for entailment that describe the 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. In the first principles, each side rules out the possibility of a world in which χ is false while φ, ψ, and the members of Γ are all true; that means that these two entailments offer equivalent guarantees, so each holds if and only if the other does. In the second principle, the sort of worlds ruled out by guarantee on the left are the worlds in which the members of Γ are all true but φ or ψ is false, and the same worlds are ruled out when we have both the guarantees on the right. The upshot is that these two principles suffice, together with the law of premises, to establish any cases of validity that depend on conjunction alone.

The if part of these principles reflects the validity of arguments of the forms Ext and Cnj (together with the chain law). The only if part of the first tells us that whatever a conjunction contributes as a premise of a valid argument is already contributed by the conclusions we could derive by Ext; that is, our use of a conjunction among the premises need only be by way of Ext. 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 themselves valid conclusions. When conjunction is the only connective employed in our analysis of sentences, applying these two principles repeatedly will eventually bring us back to arguments whose premises and conclusions are all unanalyzed components. If these components are logically independent, an argument whose premises and conclusion are drawn from them is valid when and only when its conclusion is among its premises; thus, if it is valid, its validity follows by the law of premises.

A couple of the principles for ⊤ and ⊥—those for ⊤ as a conclusion and ⊥ as a premise—assert the validity of arguments and can be used to build tree-form proofs:

The label for the second, EFQ, abbreviates the Latin ex falso quodlibet (which might be translated as from the false, whatever), a traditional description the law for ⊥ as a premise, and the label for the first, ENV, abbreviates ex nihilo verum (from nothing, the true), which gives a corresponding description of the law for ⊤ as a conclusion.

The argument ENV has no premises and serves to close off a branch of a tree, making it one that need not have a premise at its tip—as in the following proof, which shows that A, B ⇒ (B ∧ ⊤) ∧ A:

The pattern EFQ enables us to connect a proof ending with the conclucsion ⊥ to the tip of any branch. The following example uses it to show that A ∧ (⊥ ∧ B) ⇒ C ∧ D:

The premise A ∧ (⊥ ∧ B) is the starting point for proofs ending in A and B, too, but these proofs would never be needed. Even if A and B were required as premises in an argument, the proof ending with ⊥ would have been enough to yield them just as it yields C and D.

The two other laws for ⊤ and ⊥ have a different significance. The law for ⊤ as a premise does not correspond to any pattern of valid argument. It merely tells us that any proof ending with ⊤ would contribute nothing to a larger proof and may be ignored. Of course, such a proof might be connected to a branch of proof that has ⊤ at its tip; but a branch like that could be closed off by ENV instead. The law for ⊥ as an alternative does not figure as a principle governing the construction of proofs at all; recall that we have no law for ⊥ as a conclusion. Having ⊥ as a conclusion marks a proof as a proof of inconsistency, and such proofs are constructed solely by drawing conclusions from their premises.