3.3.s. Summary

The law for negation as a premise tells us two things about entailment. The first is that any conclusion is valid if and only if the denial of that conclusion can be reduced to absurdity given the premises. This is the principle of indirect proof; it is closely tied to the entailment ¬ ¬ φ ⇒ φ (and is subject to the same concerns as is that entailment). We have no need for this principle except in the case of unanalyzed components, which we will begin to call atomic sentences. And, for reasons noted later, we need to limit the use of the rule Indirect Proof (IP) to them.

Another lesson we can draw from the law for negation as a premise is that a reductio argument with a negative premise ¬ φ is valid if and only if the sentence φ is entailed by the other premises. This tells us that φ can be safely introduced as a lemma even if we drop ¬ φ from our active resources. The rule implementing this idea, Completing a Reductio (CR) serves as our rule for exploiting negative resources. It applies only to reductio arguments but the availability of IP insures that any gap will eventually turn into a gap in a reductio argument (unless it closes before that point). Since CR, by dropping a resource ¬ φ and adding a goal φ has an effect opposite to that of IP, we must apply them to different sentences φ to avoid going in circles. So, just as IP is limited to atomic sentences, CR is limited to negations of non-atomic sentences.

The rule CR can lead us to set as goals any lemmas we need to use negations in completing reductio arguments. It therefore eliminates any need for LFR.

The rule Adj is also no longer needed since the rules CR and Cnj will lead us to identify and prove any lemma that Adj would introduce. Indeed, derivations for arguments involving conjunction can now be constructed by letting the rules guide us completely. Any step that is allowed by the basic rules (that is, for now, all rules except LFR and Adj) is safe and will take the derivation some way towards completion. We call the system of derivations limited to those rules the basic system. There will often be different orders in which the basic rules can be applied, and such differences may lead to longer or shorter derivations. The use of non-basic rules can sometimes shorten derivations still further, but they may not bring a derivation any closer to is final state.

The following table collects all rules we have now seen (and, as with the table of 2.4.s, the rule labels are links to the original statements of the rules):