Normal Forms and Herbrand’s Theorem

The Gentzen calculus introduced in the last chapter provides a relatively straightforward method for demonstrating validity of first-order formulae, and one whose completeness can be proved directly. But—practically speaking—Gentzen calculi suffer quite serious disadvantages, unfortunately rendering them unsuitable for use in mechanizing proofs without extensive modification. The primary obstacles to their efficient automation are the nondeterminism, at any given stage of proof development, of the choice of rule to be applied as well as of the formula to which to apply it, and the unguided consideration of all terms for substitution in applications of the quantifier rules. In a derivation it is possible, for example, that the quantifier rules can be applied repeatedly to the same formula to the exclusion of applications of other rules needed for the successful development of a proof, or that in applying a quantifier rule, the bound variables of the formula will never be instantiated by the “right” substitution terms. We will see in Theorems 6.2.1 and 6.3.2 that restricting the syntactic forms that formulae to be proved may have, and then showing that every formula can be converted to a semantically equivalent formula meeting these syntactic requirements, will allow us to correspondingly restrict the structure of proof trees for valid formulae. From such proof trees in “standard form” we may derive significantly simpler formulae provable iff the original formulae are. This “preprocessing” of formulae in the Gentzen calculus thus emerges as a basis for deriving quite effective calculi for automating deduction. In this book, Gentzen calculi will serve primarily as a point of departure for discussing one particular class of such calculi, namely, resolution calculi, and for discussing Herbrand’s Theorem, the foundation for proving the refutation completeness of such calculi.