3.4.1. When reductios fail

The system of derivations for negation can be shown to be adequate by establishing the three properties of sufficiency, conservativeness, and decisiveness discussed in 2.3.

To say that a system is conservative is to say that all its rules are sound and safe. Soundness and safety say more than do the basic laws of negation; but, as was the case with conjunction, the natural way of establishing the basic laws for negation is enough to establish soundness and safety. The key to the argument in the laws for negation is the fact that, when it comes to separating active resources from goals, having a given sentence (φ or ¬ φ) as a resource comes to the same thing as having a contradictory sentence (¬ φ or φ, respectively) as a goal. This idea can be used to show each of the rules RAA, IP, and CR is both sound (in fact, strict) and safe, for it shows that the same counterexamples lurk in gaps to which these rules apply and in the child gaps that result from applying them. Since the rule Nc closes a gap, safety is not an issue; and, since we allow available but inactive resources to be used, we cannot expect to show strictness. But its soundness is clear: if the available resources include both φ and ¬ φ, no interpretation can make them all true, and a sound rule needs to insure some child gap is open only if the parent has a lurking counterexample that makes true all the available resources.

However, there is more to be said in the case of the properties of sufficiency and decisiveness. A system is sufficient if it has enough rules to close any dead-end gaps that have no lurking counterexamples. Given the rules we have now, a dead-end open gap must have ⊥ as its goal (since otherwise we could develop the gap with Cnj, RAA, or IP or close it with ENV), it cannot have a conjunction or a negated non-atomic sentence as a resource (since otherwise we could develop the gap with Ext or CR), it cannot have ⊥ among its resources (since otherwise we could close the gap using either QED or EFQ), and it cannot have both a sentence and its negation among its resources (since otherwise we could close the gap with Nc). So the proximate argument of a dead-end gap must be a reductio whose premises are limited to ⊥, atomic, and negated atomic sentences, with no sentence appearing both negated and unnegated among the premises. To show sufficiency, we must show that we can always separate the premises of such an argument from its conclusion. And we can do this by making an atomic sentence true when it appears among the premises and false when its negation appears. We can assign truth values in this way since no sentence appears both negated and unnegated, and an assignment like this will make all premises true and it will, of course, make the conclusion ⊥ false.

This argument for sufficiency tells us what we need to do in order to confirm a counterexample on the basis of a dead-end open gap. Here is an example of that.

(Although this derivation has been continued as far as possible, it could have been ended after the dead-end gap appeared at stage 4.)

The proximate argument of the dead-end gap is ¬ A, ¬ B / ⊥. To separate the premises from the conclusion, we must make A and B false since their negations are active resources of the dead-end gap. The value assigned to C does not matter since neither it nor ¬ C appears among the premises of this argument. So, although C is assigned T in the counterexample confirmed above, an interpretation that made each of A, B, and C false would also be a counterexample.

The basic issues regarding decisiveness were touched on when the rule IP was introduced in 3.3.1, but they deserve to be considered a little more fully. The system of derivations for conjunction is easily seen to be decisive because we cannot go on forever dropping and shortening sentences among the resources and goals. But we now have rules that can do things other than simplifying the resources and goals. In particular, we can add resources while dropping goals and vice versa, and, in the case of IP, we can do this by adding a resource that has one more connective than the goal that was dropped. The cases where we use IP and CR have been restricted so that we cannot go in circles, but an argument is needed to show that those restrictions are enough.

Decisiveness will follow if all our rules are progressive in the sense of bringing us closer to a dead end in a way that cannot be continued indefinitely. In judging this, we cannot now look only at the number of connectives in sentences. In the first place, atomic sentences have no connectives, but are a sign that a derivation has not reached its end when they appear as goals. And, second, negated atomic sentences do contain connectives but can appear as resources in a dead-end gap. Let us say that the sort of sentences that may appear in a gap that has reached a dead end are minimal. Then a minimal resource will be ⊤ or an atomic or negated atomic sentence and a minimal goal must be ⊥. Thus whether a given sentence counts as minimal depends on whether it appears as a resource or a goal.

In order to measure distance from the end of a derivation, we will assign each resource and goal a grade. Minimal sentences form the lowest grade, and non-minimal sentences are graded above them and relative to one another by counting the connectives appearing in them. There are many ways of assigning numerical grades that would accomplish this. To be concrete, let us suppose we assign grade 0 to minimal sentences and then one more than the number of connectives to any other sentence. So atomic and negated atomic resources both have grade 0, but atomic and negated atomic goals have grades 1 and 2, respectively. As a goal, ⊥ has grade 0 while, as a resource, it has grade 1. (Notice also that, while ⊤ has grade 0 as a resource and grade 1 as a goal, its negation ¬ ⊤ has grade 2 whether it is a resource or a goal.)

Now, consider the whole group of active resources and goals of every open gap of a derivation. If we look at each of the rules for developing gaps, we see that the effect of applying any one of them will always be to eliminate an active resource or a goal. It may also add resources or goals, but any sentence that is added either has fewer connectives than the sentence dropped or, in the case of IP, is a minimal sentence when the sentence dropped was not minimal. Either way, additions will be sentences of a lower grade, so eventually all active sentences will be minimal and the process must end. Notice that if, for example, we allowed CR to apply to negated atomic sentences as well as negated non-atomic sentences, this rule would no longer be progressive since we could, for example, drop a minimal resource ¬ A and add the non-minimal goal A. However, when φ is not atomic, ¬ φ has a higher grade than φ because of the extra connective, so the restricted CR is progressive.