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. Here we will look at these properties in the case of the current system. To say that the 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 the natural way of establishing the basic laws for negation is enough to establish soundness and safety. The key to the argument in both cases is the fact that, when it comes to dividing a gap, having a given sentence (φ or ¬ φ) as a resource comes to the same thing as having a contradictory sentence (¬ φ or φ, respectively) as a goal. However, there is more to be said in the case of the properties of sufficiency and decisiveness.
The system is sufficient if it has enough rules to close any dead-end gaps that cannot be divided. Given the rules of the current system, 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 compound 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. We can divide such an argument 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, such an assignment will make all premises true, and the conclusion is bound to be false since it is ⊥.
This argument for sufficiency tells us what we need to do in order to present a counterexample on the basis of a dead-end open gap. Here is an example of that.
│¬ (A ∧ ¬ (B ∧ C)) | 2 | |
│¬ B | (7) | |
├─ | ||
││¬ A | ||
│├─ | ||
│││││¬ A | ||
││││├─ | ||
│││││○ | ¬ A, ¬ B ⇏ ⊥ | |
││││├─ | ||
│││││⊥ | 4 | |
│││├─ | ||
4 IP | ││││A | 3 |
│││ | ||
│││││B ∧ C | 6 | |
││││├─ | ||
6 Ext | │││││B | (7) |
6 Ext | │││││C | |
│││││● | ||
││││├─ | ||
7 Nc | │││││⊥ | 5 |
│││├─ | ||
5 RAA | ││││¬ (B ∧ C) | 3 |
││├─ | ||
3 Cnj | │││A ∧ ¬ (B ∧ C) | 2 |
│├─ | ||
2 CR | ││⊥ | 1 |
├─ | ||
1 IP | │A |
A | B | C | ¬ | (A | ∧ | ¬ | (B | ∧ | C)) | , | ¬ | B | / | A |
F | F | T | Ⓣ | F | T | F | Ⓣ | Ⓕ |
(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 divide this, 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 presented above, an interpretation that made each of A, B, and C false would also be a counterexample.
Finally, recall that a system is decisive if we cannot go on applying its rules forever—i.e., if we must always reach a point at which no more rules can be applied. We argued that the system of derivations of the last chapter was decisive because we could not 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, adding resources while dropping goals and vice verse and, in the case of IP, doing this by adding a resource more complex than the goal that was dropped. The cases where we use IP and CR were restricted so that we would not go in circles, but some argument is needed to show that those restrictions were enough.
Decisiveness will follow if all our rules are progressive on some measure of distance from the end of a derivation. We cannot measure this simply by the length of the goal and resources of a gap since, in the first place, atomic sentences are as short as possible, but are a sign that a derivation has not reached its end when they appear as goals. And, on the other hand, negated atomic sentences are not as short as possible but can appear as resources at the end of a derivation. Let us say that the sort of sentences that may appear in a gap that cannot be narrowed further are minimal; that is, a minimal resources will be ⊤ or an atomic or negated atomic sentence and a minimal goal must be ⊥. Notice that 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 according to their length. 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 narrowing 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 as goals, but any sentence that is added either is shorter 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 compounds, this would no longer be true since we would drop a minimal resource ¬ φ and add a non-minimal goal φ. However, when φ is compound, ¬ φ has a higher grade than φ because it is longer, so the change can be seen as progressive.