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 divide 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 divide 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 alternatives divided—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 sequent proofs:

That is, moving from the root to the two branches, we exploit φ ∨ ψ and thus drop it from the active resources, and we add assumptions φ and ψ by introducing suppositions φ and ψ with separate scope lines. The goal of the parent gap is carried over to each of its two children. The rule is safe because any interpretation dividing one of the children is bound to 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 from the parent to the children. And the rule is strict because any interpretation dividing the parent must, in order to make φ ∨ ψ true, make true at least one of φ and ψ.

As in other cases, the use of numerical annotations in PC reflects the corresponding rule for tree-form proofs:

The conclusion χ is based on three premises (two with assumptions that are discharged when we draw this conclusion), so in derivations the stage number appears on the right of three lines, 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 tree-form proofs 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 separate the proof of a claim from 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 tree-form proofs also makes it clear that, apart from the separation of φ and ψ, the form of PC is much like that of Lem, but there is an important difference in the way they are employed in proofs. The rule Lem would be used to initiate the search for a proof of its first premise. But, while the tree-form 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 sequent proofs.