When a derivation is constructed for an invalid argument, we eventually reach a point where an open gap has reached a dead end without closing. We mark such a gap with a empty circle ○ and write its active resources and goal with the sign ⊭ between to indicate that they do not form a valid argument. And we will see that the invalidity of the proximate argument of a dead-end gap implies the invalidity of the ultimate argument for which the derivation is constructed.

We will often be concerned with formal validity, so we extend to assignments of truth values the ideas of dividing premises from a conclusion and of constituting a counterexample to an argument. And we speak of a gap being divided when its proximate argument is. The fact that any dead-end open is divided—that its proximate argument has a counterexample—indicates that our system is sufficient in the sense of having enough rules to close all dead-end gaps whose proximate arguments are valid.

When speaking of the tree structure of the gaps of a proof, it is convenient to use a genealogical metaphor and to speak of a gap at one stage as the parent of the gaps that derive from it at the next stage, gaps that are its children. Children of a gap’s children, their children, and so on are descendants of the gap, and it is an ancestor of them. We can state a necessary and sufficient condition for the divisbility of a gap in terms of the existence of divisible descendants at later stages.

We can be sure that a counterexample to the proximate argument of a dead-end gap is a counterexample to the derivation’s ultimate argument provided all our rules are safe in the sense of never introducing new ways of dividing gaps. When the converse is true, when we our rules never allow us to ignore ways that a gap might be divided, they are strict. Since our real interest is in the ultimate argument of a derivation, it is really enough to attend to dividing intepretations when they also divide all ancestors of a gap. Rules that insure that we do this are sound; when all rules are safe, sound rules are also strict. The idea of soundness enables us to justify the use of available but inactive resources (to, for example, close gaps) even when not all rules are safe. A system whose rules are all sound and also safe is conservative.

When a dead-end open gap is divided by an interpretation, this interpretation is also a counterexample to the ultimate argument of the derivation, and we will present such a counterexample as a way of finishing off a derivation that fails.

A system will be decisive (in the sense that any derivation will always come to an end) provided its rules are all progressive (in the sense of always leading us closer to a point where no more can be done). Many rules are progressive because they either close a gap or replace a goal or active resource by one or more simpler sentences. A decisive system which is sufficient and conservative (and is therefore correct in the answers it gives) provides a decision procedure for formal validity.

Not all systems we consider will provide decision procedures but all will be sound in the sense of providing proofs only for valid arguments and complete in the sense of leading us to a proof whenever an argument is formally valid.

An argument that is valid may have a form that is invalid in the sense that some intensional interpretation of the unanalyzed components appearing in the form—i.e., some way of associating actual sentences with them—yields an invalid argument. Formal validity implies validity, so a derivation that succeeds shows both, but one that fails only shows formal invalidity.