Modern Logic: From Frege to Gödel: Herbrand
MODERN LOGIC: FROM FREGE TO GÖDEL: HERBRAND
Despite a tragically short life—he was killed in a mountaineering accident in 1931 at the age of twenty-three—Jacques Herbrand made substantial contributions to the development of mathematical logic, especially to investigations in the metatheory of logic that were the particular concern of Hilbert and his school. The bulk of Herbrand's contributions is to be found in his University of Paris dissertation of 1930, Recherches sur la théorie de la démonstration (published in Travaux de la Société des Sciences et des Lettres de Varsovie, Classe III (33) [1930]: 33–160). This work has much in common with the later "Untersuchungen über das logische Schliessen" of Gerhard Gentzen, but the presentation of proofs and explanations is much less perspicuous than Gentzen's, and even now some aspects of Herbrand's work await further clarification and elaboration.
Herbrand's starting point is the system of classical propositional logic presented in Whitehead and Russell's Principia Mathematica, but the extension of this to functional calculi of first and higher orders is effected by the addition of further rules in place of axioms. The resultant calculi, in which mathematical theories may be embedded, are investigated from a Hilbertian proof-theoretic viewpoint, with emphasis on such syntactic notions as derivability and to the exclusion of semantic questions that cannot be given a finistic interpretation. New proofs are given of a number of results already known, such as those concerning solvable cases of the decision problem, and for the first time the idea and proof of the deduction theorem is presented for a particular system of logic. That is, Herbrand showed that a necessary and sufficient condition for the derivability of a proposition P in his theory with hypotheses H is that H ⊃ P should be derivable in the logic without hypotheses.
Herbrand's most powerful result concerns the necessity and sufficiency of certain conditions for the provability of a quantificational schema. He showed, in fact, that such a schema is provable if and only if a quantifier-free tautology of a prescribed form is constructible from it. The proofs of the various theses that go to make up this result are somewhat complicated, but the form of tautology which is associated with a provable formula can be indicated in the following way: First, a given quantificational schema is so transformed that each quantifier has its minimum scope or, alternatively, each has its maximum scope. Taking just the first case, then, all the quantifiers are placed initially and have a scope that extends to the far right of the formula.
Suppose we are given a schema in this form—for example, ∃x ∃y ∀z [Fx → (Fy & Fz )]—which we shall call "A." The necessary and sufficient condition of A 's holding is that it be false that for any x and y there is a value of z for which the matrix of A is false. Accordingly, if x and y both take the value a 1, say, there must be some value a 2 of z that results in the falsity of the matrix if A is to be false; further, if x takes the value a 1 and y takes the value a 2, then for some value a 3 of z the matrix must be false; again, if x takes the value a 2 and y takes the value a 1, the matrix must be false for some value a 4 of z, and so on. But if we find that at least one of the substitution instances of the matrix so generated must be true, we have shown the failure of a necessary condition for the falsity of A. In fact, this is the outcome of the present example, since the disjunction of the cases so far considered, [Fa 1 → (Fa 1 & Fa 2)] ∨ [Fa 1 → (Fa 2 & Fa 3)] ∨ [Fa 2 → (Fa 1 & Fa 4)], is a tautology—thus, if Fa 2 is true, the first disjunct is true, and if Fa 2 is false, the last disjunct is true.
Herbrand showed how such disjunctions can be constructed from a formula in prenex normal form with the quantifiers occurring in any number and order. He showed, too, that the original formula can be retrieved from such a disjunction by the application of a few simple rules, without use of modus ponens. And, indeed, it is clear from the example given that the only rules required for the derivation of the original formula from the tautology are rules allowing for the insertion of quantifiers before the disjuncts and a rule allowing us to erase repetitions of identical disjuncts. The final result allows us to assert that the constructibility of a tautologous disjunction is both a necessary and a sufficient condition for the provability of the associated quantified schema.
In addition to shedding considerable light on the structure of quantification theory, Herbrand's theorem is the source of a number of important metatheoretic results. Löwenheim's theorem is an immediate consequence—accepted by Herbrand only when reinterpreted finitistically—and certain cases of the decision problem allow of simple resolution. Important for Herbrand's aims was the application of his theorem to the question of the consistency of arithmetic, and he was able to show that if we have a model for a set of hypotheses, an interpretation with respect to some domain under which all these hypotheses are true, then no contradiction can arise in the theory deduced from the axioms. Suppose hypotheses H 1, H 2, · · ·, Hn give rise to a contradiction while having a true interpretation within the model. Since H 1, & H 2 & · · · & Hn comes out true in the model, the model brings the negation of this conjunction out false, and if a formula is false in some domain, it is not associated with a quantifier-free tautology. If, on the other hand, H 1, H 2, · · ·, H n yield a contradiction, then ∼(H 1 & H 2 & · · · & H n ) is provable and thus is associated with a tautologous disjunction. This form of consistency proof was discussed further by Herbrand in his later article "Sur la Non-contradiction de l'arithmétique" (Journal für die reine und angewandte Mathematik 166 [1931]: 1–8), and the same idea appears in Gentzen's "Untersuchungen über das logische Schliessen."
See also Quantifiers in Formal Logic; Russell, Bertrand Arthur William; Whitehead, Alfred North.
Bede Rundle (1967)