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.2. 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.

It is not hard to see that this process will work for any valid argument that depends on conjunction alone. By working backward from its conclusion using Cnj arguments we can grow a tree which will eventually have the ultimate components of the conclusion at the tips of its branches. Call this an analysis tree. By applying Ext arguments repeatedly to our premises, we will eventually have a series of chains, each beginning with the premises and ending with one of the ultimate components of a premise, with all such components represented among the chains. Call these exploitation chains. Applying this approach to the example above, we would have three exploitation chains in addition to the analysis tree.

We can then construct the proof shown above by pasting the end of each analysis chain over the tip of one of the branches of the analysis tree. In this case, the chains match up one to one with the tips of branches; but, in other cases, we might need to use more than one copy of a given chain, and we might not need to use some chains at all. All that is required to complete a proof is that the tip of each branch be matched by some chain, and that could fail to happen only if the conclusion contained an ultimate component that was not an ultimate component of any of the premises. But an argument whose conclusion contained an ultimate component not appearing in the premises would not be valid because, by making this component false and all others true, we would make the conclusion false while making the premises true. And, if the ultimate components of the premises and conclusion form a set that is logically independent (in the sense discussed in 1.4.6), this sort of assignment of truth values would correspond to some possible world. So if a relation of entailment holds solely in virtue of the way sentences are formed using conjunction (and not in virtue of logical relations among their ultimate components), it can be shown to hold by the sort of proofs we have been considering.

The way we have shown this will not work when we consider proofs involving 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 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.

The recipe for constructing tree-form proofs that we looked at earlier had us put together an analysis tree and exploitation chains by pasting the ends of the latter onto the tips of the former’s branches. It will help in comparing the tree-form proofs to those we will go on to consider if we have a pattern of argument to use as the glue, so we will add a pattern reflecting the reflexivity of implication:

The name for this abbreviates the Latin phrase quod erat demonstrandum, which might be translated as what was to be proven. This Latin phrase is traditionally used when a planned conclusion is reached. The use of the pattern QED is illustrated in the following example, which establishes that (A ∧ B) ∧ C, D ⇒ C ∧ (A ∧ D).

Tree-form proof

Notice that this proof uses only two of the three chains of extractions that begin with the first premise.

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 an analysis tree, making it one that need not have an exploitation chain connected to it—as in the following proof, which shows that A, B ⇒ (B ∧ ⊤) ∧ A:

The pattern EFQ enables us to connect an exploitation chain ending with ⊥ 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 exploitation chains ending in A and B, too, but even if these sentences had appeared at the tips of branches of an analysis tree, the exploitation chain ending with ⊥ would have been enough to complete the proof.

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 an exploitation chain ending with ⊤ contributes nothing to a proof and may be ignored. Of course, such a chain might be connected to a branch of an analysis tree that has ⊤ at its tip; but such a branch 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. Because its two sides have different numbers of alternatives, it does not provide a way of restating claims of entailment: if one side has a single alternative and thus counts as claim of entailment, the other will either have no alternatives or more than one.