ABSTRACT
The Completeness Theorem for first-order trees, which with the corresponding Soundness Theorem will be proved in section 3, says that every open branch in a finished tree generated by a finite set Σ of sentences determines a model of Σ. It follows that if Σ is inconsistent, then every finished tree closes. If a tree closes, it closes after finitely many steps. In practice, we want to use the theorem to justify the following conditional: if a finite set is inconsistent, then it will generate a closed tree. Granted the truth of that (meta)conditional, we should then have a partial decision procedure for inconsistency: if a set Σ is inconsistent, then eventually we shall be able to tell it is because any tree generated from it will close (the procedure is only partial because if the tree is not going to close, i.e. if Σ is consistent, we may never know).
