## Thèses présentées à la Faculté des Sciences de Paris pour obtenir le grade de Docteur ès Sciences Mathématiques. 1re thèse: Recherches sur la théorie de la démonstration. 2me thèse: Propositions données par la faculté. Soutenues le 1930 devant la commission d'examen.

Warsaw: Dziewulski, 1930.

First edition, rare, and a fine copy in the original printed wrappers, of Herbrand’s doctoral dissertation, written in 1929 as a contribution to Hilbert’s programme. Bernays described Herbrand’s theorem as “the central theorem of predicate logic”, and van Heijenoort wrote that “[Frege’s] *Begriffsschrift* (1879)*,* Löwenheim’s paper [‘Über Möglichkeiten im Relativkalkül,’ 1915], and Chapter 5 of Herbrand’s thesis [containing Herbrand’s theorem] are the three cornerstones of modern logic.” “Herbrand had created a significant part of the world heritage of modern logic when he died in 1931” (Wirth). “Herbrand gave early signs of his mathematical gifts, entering the École Normale Supérieure at the exceptional age of seventeen and ranking first in the entering class. He completed his doctoral dissertation in April 1929. That October he began a year of service in the French army. He then went to Germany on a Rockefeller fellowship, studying in Berlin (until May 1931) with John von Neumann, then in Hamburg (May-June) with Emil Artin, and in Göttingen (June-July) with Emmy Noether. He left Göttingen for a vacation in the Alps and a few days later was killed in a fall at the age of twenty-three … Herbrand’s main contribution to logic was what is now called the Herbrand theorem, published in his doctoral dissertation: it is the most fundamental result in quantification theory” (DSB). “Herbrand’s theorem establishes a link between quantification theory and sentential logic which is important in that it gives a method to test a formula in quantification theory by successively testing formulas for sentential validity. Since testing for sentential validity is a mechanical process, Herbrand’s theorem is today of major importance in software developed for theorem proving by computer” (MacTutor). “Consider an arbitrary formula *F* of quantification theory, then delete all its quantifiers and replace the variables thus made free with constants selected according to a definite procedure. A lexical instance of *F* is thus obtained. Let *F _{i}*be the

*i*th lexical instance of

*F*, the instances being generated in some definite order. The Herbrand theorem states the

*F*is provable in anyone of the (equivalent) systems of quantification theory if and only if for some number

*k*the disjunction

*F*

_{1}v … v

*F*(now called the

_{k}*k*th Herbrand disjunction) is sententially valid. The Herbrand theorem establishes an unexpected bridge between quantification theory and sentential logic. Testing a formula for sentential validity is a purely mechanical operation. Given a formula

*F*of quantification theory, one tests the

*k*th Herbrand disjunction of

*F*successively for

*k*= 1,

*k*= 2, and so on: if

*F*is provable, one eventually reaches a number

*k*for which the

*k*th Herbrand disjunction is valid. If

*F*is not provable, there is, of course, no such

*k*, and one never learns that there is no such

*k*(in accordance with the fact that there is no decision procedure for quantification theory). Besides yielding a very convenient proof procedure, the Herbrand theorem has many applications (a field explored by Herbrand himself) to decision and reduction problems and to proofs of consistency. Almost all methods for proving theorems by machine rest upon the Herbrand theorem” (DSB). ABPC/RBH list only one copy.

“Herbrand’s principal concern in his logical writings was to develop a unified approach to all questions of proof theory … In addition to providing both information about the structure of logical proofs and a method for obtaining consistency and decidability results, this theorem also furnished constructive insight into nonconstructive notions such as satisfiability … In order to appreciate fully the importance of his results and their place in the history of logic, it is helpful to trace the major influences on Herbrand’s work: Whitehead and Russell’s *Principia mathematica*, Löwenheim (1915) and Skolem [‘Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen’, 1920], and the articles of the Hilbert school which appeared during the 1920s.

“Herbrand took the *Principia mathematica* to furnish experimental evidence that classical mathematics can in fact be codified in a formal system using a small number of primitive signs and rules of inference. The possibility of such a formalization shows the importance of metamathematical investigations. Herbrand says: ‘It becomes natural to study this system of signs in itself, and to pose problems regarding it. The solution of these will have an immediate echo in our general knowledge of mathematics.’ Herbrand begins his thesis by examining the propositional calculus of the *Principia*, and then takes great pains to show that his formulation of quantification theory is equivalent to that used by Whitehead and Russell. Moreover, one of the methods Whitehead and Russell use to construct quantificational logic seems to be the source of two key concepts in Herbrand, namely, those of normal identity and property A.

“Löwenheim’s paper of 1915 contains a number of ideas central to much subsequent work. He uses a notion of a universe of discourse susceptible to change, a notion coming from the Boole-Peirce-Schröder tradition. Löwenheim completely ignores syntactic considerations such as provability; rather, he assumes a naïve notion of a formula’s being true in a universe under a given interpretation of the predicate letters. Thus, the (set-theoretic) notions of validity and satisfiability come into play. Using them, Löwenheim proves his well-known theorem: If a formula of quantification theory with identity is satisfiable, then it is satisfiable in a denumerable universe … Löwenheim’s proof is very informal and difficult to follow … Skolem later gave rigorous proofs …

“The method of investigation that Herbrand adopts was essentially due to Hilbert. Partially in response to Brouwer’s critique of classical mathematics, Hilbert developed his notion of proof theory. The proof theorist’s task is to examine formal systems as systems of signs, divorced from any intuitive content. The methods used must be purely finite … The most important questions in Hilbert’s metamathematics concern characterizations of provability in given formal systems; central among these are problems of consistency, completeness and decidability. Herbrand’s logical work is entirely within this framework; he agrees that arguments about formal systems must be finitistic, and is concerned with the problems Hilbert raises. In the Introduction to [his thesis] Herbrand explains this concept of metamathematics, but he ignores the more obscure epistemological views of Hilbert and Brouwer. Instead, he bases the restriction to finitistic reasoning on the need, in the face of critiques of infinite totalities and the law of the excluded middle, for a logical method satisfying ‘requirements of the most absolute rigor.’

“From the finitistic viewpoint, the naïve notion of truth is suspect; Hilbert and Herbrand ask what finite sense can be given in general to the attribution of truth in an infinite universe to a formula with quantifiers. The objection to quantifiers arises primarily from the fact that in the intuitive semantics of quantification theory, the existential quantifier is often interpreted as standing for a choice function … The proof-theoretic program was based on Hilbert’s insight that in any given proof only a finite amount of knowledge of this choice function is required … Von Neumann’s consistency proof for a weal system of arithmetic (1927) takes this form … In Chap. 4 of [his thesis], Herbrand presents a simpler and more powerful proof using the same underlying idea. By certain mechanical instantiations of numerals for quantified variables, he finds a quantifier-free equivalent *P’* for every formula *P* of a similar weak system of arithmetic. Furthermore, *P* is provable in this system if and only if *P’ *is provable in a quantifier-free subsystem … Herbrand calls *P’* the ‘réduite’ (literally, reduction) of *P*, thus emphasizing his aim of reducing provability using quantifiers to provability without quantifiers” (*Jacques Herbrand. Logical Writings*, van Heijenoort (ed.), pp. 1-4).

“Herbrand’s ideas have yielded numerous metamathematical applications. The normal form for proofs supplies a tool for obtaining consistency proofs. Furthermore, the elimination of quantifiers in favour of functional terms suggests how to exhibit the constructive content of a formal theory … Herbrand’s theorem also allows us to prove a theory consistent by approximating a model for it … Herbrand himself gave a consistency proof for a fragment of arithmetic along these lines, and his methods have been extended to yield proofs for the full system … Finally, Herbrand’s theorem supplies an approach to the decision problem [the ‘Entscheidungsproblem’] for classes of quantificational formulas, that is, to discovering an algorithm which, for any formula in the class, computes whether or not it is satisfiable. The idea here is to investigate the relationship between syntactic properties of quantificational formulas and the structure of their expansions, and to discover properties of the latter which ensure the existence of a decision procedure. His theorem and the methods introduced in its proof are relevant not only to theoretical decidability results, but also to the design of implementable automated reasoning procedures. These employ unification algorithms to improve the efficiency of testing quantifier-free expansions for satisfiability, and Herbrand is credited with being the first to derive such an algorithm” (*Routledge Encyclopedia of Philosophy*: *Genealogy to Iqbal*, p. 377).

Buss points out that Herbrand’s thesis also includes a construction that is very close to the completeness theorem for first-order logic. (Recall that the completeness theorem was first proved by Gödel in 1930, in the same year that Herbrand’s thesis was completed.) In fact, Buss argues, Herbrand *could* have proved the completeness theorem using the techniques in his thesis but declined to do so because he would have had to invoke the Axiom of Choice. Herbrand took a very strong constructive, formalist point of view, and he would have rejected non-constructive arguments on philosophical grounds.

Bernays. ‘Über den Zusammenhang des Herbrandschen Satzes mit denneueren Ergebnissen von Schütte und Stenius,’ *Proceedings of the International Congress of Mathematicians 1954*, Vol. II (1957), p. 397. Buss, ‘On Herbrand’s Theorem,’ *Logic and Computational Complexity, Lecture Notes in Computer Science* 960 (1995), pp. 195-209. Van Heijenoort, ‘Logic as a calculus and logic as a language,’ *Synthese* 17 (1967), 324–330. Wirth, ‘Herbrand’s Fundamental Theorem in the Eyes of Jen van Heijenoort,’ *Logica Universalis* (2012), pp. 485–520.

8vo (239 x 169 mm), pp. [ii], 128, [2]. Original printed wrappers (first and last page a little browned).

Item #5040

**
Price:
$2,850.00
**