When a derivation is constructed for an invalid argument, eventually we will find that 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 idea of constituting a counterexample to an argument. The fact that any dead-end open gap has its active resources separated from its conclusion by some interpretation 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 a counterexample to its proximate argument lurk in a gap in terms of the existence of lurking counterexamples 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 lurking counterexamples. When the converse is true, when we our rules never allow us to ignore lurking counterexamples, they are strict. Since our real interest is in the ultimate argument of a derivation, it is really enough to attend to lurking counterexamples when they also lurk in 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 an interpretation is a counterexample to the proximate argument of a dead-end open gap, this interpretation is also a counterexample to the ultimate argument of the derivation, and we will confirm 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.