4.2.1. Proofs by cases

The validity of the argument

can be accounted for by the validity of the following two arguments:

Each replaces the disjunctive third premise of the original argument by one of its two components. This way of establishing an entailment is sometimes called a proof by cases. In this example, the two cases are Sam having praised the proposal and Sam having condemned it. Since the disjunction says all and only what is common to these two claims, what follows from the disjunction in isolation or in addition to other premises is what follows from each of these claims under similar circumstances.

More formally, the idea behind proofs by cases is captured by this principle:

To see why this law is true note that to separate the members of Γ and φ ∨ ψ on the one hand from χ on the other, a possible world must make φ ∨ ψ and all members of Γ true while making χ false. To do this it must make at least one of φ and ψ true, so it must provide a counterexample to at least one of the arguments Γ, φ / χ and Γ, ψ / χ. So, to say that the original argument is valid is to say that neither of these latter arguments can have its premises and conclusion separated—that is, that both are valid.

This idea appears in derivations by way of a rule we will call Proof by Cases (PC); it is shown in Figure 4.2.1-1.

PC divides a gap into two new gaps. Each is a case argument that retains the original goal but adds one of the components of the disjunction as a supposition. The function of each supposition is to specify one of the two sorts of case in which the original disjunction is true. A supposition is required because, although our premises tell us that at least one of the disjuncts is true, we do not know which that is and the one that is true will vary among the possible worlds in which the premises are all true.

The safety and soundness (indeed, strictness) of this rule is shown by its effect on proximate arguments, which follows the pattern of law for disjunction as a premise understood as a rule for argument trees:

That is, moving left to right, we exploit φ ∨ ψ and thus drop it from the active resources, and we add suppositions φ and ψ. The goal of the parent gap is carried over to each of its two children. The rule is safe because any counterexample lurking in one of the children is bound to lurk in the parent, too. It must make the resources of the parent true because φ ∨ ψ is implied by each of φ and ψ, and the requirement to make χ false remains unchanged as we move between the parent and the children. Moverover, the rule is strict because any counterexample lurking in the parent must, in order to make φ ∨ ψ true, make at least one of φ and ψ true also, so it will lurk in at least one of the children.

As in other cases, the use of numerical annotations in PC reflects the corresponding rule for conclusion trees, which is shown here as a transition from one stage in the construction of the tree to the next.

φ ∨ ψ ? χ

→

φ ∨ ψ φ ? χ ψ ? χ PC χ

The conclusion χ is based on three premises (one that we have found among the resources and two more we plan to reach), so in derivations the stage number appears on the right of three lines, the the disjunction that is exploited and the goals of the two new scope lines.

Here is a derivation which uses derivation rule to provide a proof for the example with which we began.

In the two case arguments, we suppose first that Sam praised the proposal and then that he condemned it and, in each case, we show that he granted the proposal’s significance (by showing that he could not have failed to grant it). Since at least one of these two cases must be true whenever the premises are all true, we know that the conclusion must be true also.

The rule for conclusion trees displayed above shows that PC represents a new function for suppositions. Like Lem (or the special case LFR) on the one hand and RAA and IP on the other, we use suppositions in PC to consider the consequences of claims without asserting them. But, while we did this in RAA and IP in order to show the suppositions were false and in Lem and LFR in order to consider the proof of a claim independently of the investigation of its consequences, we do it here to consider separately the consequences of two alternatives without deciding which of the two is true.

The rule for conclusion trees also makes it clear that, apart from the separate consideration of φ and ψ, the form of PC is much like that of Lem. But there is an important difference in the way these rules are employed in proofs. The rule Lem would be used to initiate the search for a proof of its first premise. On the other hand, while the conclusion-tree rule PC might be used in this way, we use PC in derivations instead to derive consequences from a premise φ ∨ ψ that has already been established, and that aspect of the derivation rule is better reflected in the rule for argument trees shown earlier, which displays less analogy with the argument-tree rule for Lem.