Lectures on Jacques Herbrand as a Logician

Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller, Serge Autexier

SEKI Report SR–2009–01

SEKI Report http://www.dfki.de/seki ISSN 1437-4447

SEKI is published by the following institutions:

German Research Center for Artificial Intelligence (DFKI GmbH), Germany

• Robert Hooke Str. 5, D–28359 Bremen
• Trippstadter Str. 122, D–67663 Kaiserslautern
• Campus D 3 2, D–66123 Saarbrücken

International University of Germany, Campus 1, D–76646 Bruchsal, Germany

Jacobs University Bremen, School of Engineering & Science, Campus Ring 1, D–28759 Bremen, Germany

Universität des Saarlandes, FR 6.2 Informatik, Campus, D–66123 Saarbrücken, Germany

SEKI Editor:

Claus-Peter Wirth

E-mail: wirth@logic.at
WWW: http://www.ags.uni-sb.de/~cp

Please send surface mail exclusively to:

DFKI Bremen GmbH Safe and Secure Cognitive Systems Cartesium Enrique Schmidt Str. 5 D–28359 Bremen Germany

This SEKI Report was internally reviewed by:

Irving H. Anellis Indiana University – Purdue University Indianapolis

E-mail: irvanellis@lycos.com
WWW: http://irvinganellis.blogspot.com

Paolo Bussotti Centro Studi Enriques, Livorno

E-mail: bussottipaolo@yahoo.com

Lawrence C. Paulson Computer Laboratory, University of Cambridge, UK

E-mail: lp15@cam.ac.uk
WWW: http://www.cl.cam.ac.uk/~lp15

Lectures on Jacques Herbrand as a Logician

Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller, Serge Autexier

Definitive Print Edition Submitted December 13, 2007 February 25, 2009

Abstract

We give some lectures on the work on formal logic of Jacques Herbrand, and sketch his life and his influence on automated theorem proving. The intended audience ranges from students interested in logic over historians to logicians. Besides the wellknown correction of Herbrand’s False Lemma by Gödel and Dreben, we also present the hardly known unpublished correction of Heijenoort and its consequences on Herbrand’s Modus Ponens Elimination. Besides Herbrand’s Fundamental Theorem and its relation to the Löwenheim–Skolem Theorem, we carefully investigate Herbrand’s notion of intuitionism in connection with his notion of falsehood in an infinite domain. We sketch Herbrand’s two proofs of the consistency of arithmetic and his notion of a recursive function, and last but not least, present the correct original text of his unification algorithm with a new translation.

Keywords: Jacques Herbrand, History of Logic, Herbrand’s Fundamental Theorem, Modus Ponens Elimination, Löwenheim–Skolem Theorem, Falsehood in an Infinite Domain, Consistency of Arithmetic, Recursive Functions, Unification Algorithm.

Contents

1 Introductory Lecture 3 2 Herbrand’s Life 9 3 Finitistic Classical First-Order Proof Theory 11 4 Herbrand’s Main Contributions to Logic and

his Notion of Intuitionism 15 5 The Context of Herbrand’s Work on Logic 17 6 A Genius with some Flaws 18 7 Champs Finis, Herbrand Universe, and Herbrand Expansion 20 8 Skolemization, Smullyan’s Uniform Notation,

and γ- and δ-quantification 21 9 Axioms and Rules of Inference 24 10 Normal Identities, Properties A, B, and C, and

Herbrand Disjunction and Complexity 26 11 Herbrand’s False Lemma 28 12 The Fundamental Theorem 30 13 Modus Ponens Elimination 32 14 The Löwenheim–Skolem Theorem and

Herbrand’s Finitistic Notion of Falsehood in an Infinite Domain 35 15 Herbrand’s First Proof of the Consistency of Arithmetic 40 16 Herbrand’s Second Proof of the Consistency of Arithmetic 41 17 Foreshadowing Recursive Functions 43 18 Herbrand’s Influence on Automated Deduction and

Herbrand’s Unification Algorithm 45 19 Conclusion 49 Acknowledgements 50 Bibliography of Jacques Herbrand 51 References 55 Index 67

1 Introductory Lecture

Regarding the work on formal logic of Jacques Herbrand (1908–1931), our following lectures will provide a lot of useful information for the student interested in logic as well as a few surprising insights for the experts in the fields of history and logic.

As Jacques Herbrand today is an idol of many scholars, right from the start we could not help asking ourselves the following questions: Is there still something to learn from his work on logic which has not found its way into the standard textbooks on logic? Has everything already been published which should be said or written on him? Should we treat him just as an icon?

Well, the lives of mathematical prodigies who passed away very early after groundbreaking work invoke a fascination for later generations: The early death of Niels Henrik Abel (1802–1829) from ill health after a sled trip to visit his fiancé for Christmas; the obscure circumstances of Evariste Galois’ (1811–1832) duel; the deaths of consumption of Gotthold Eisenstein (1823–1852) (who sometimes lectured his few students from his bedside) and of Gustav Roch (1839–1866) in Venice; the drowning of the topologist Pavel Samuilovich Urysohn (1898–1924) on vacation; the burial of Raymond Paley (1907–1933) in an avalanche at Deception Pass in the Rocky Mountains; as well as the fatal imprisonment of Gerhard Gentzen (1909–1945) in Prague^{1} — these are tales most scholars of logic and mathematics have heard in their student days.

Jacques Herbrand, a young prodigy admitted to the École Normale Supérieure as the best student of the year 1925, when he was 17, died only six years later in a mountaineering accident in La Bérarde (Isère) in France. He left a legacy in logic and mathematics that is outstanding.

Despite his very short life, Herbrand’s contributions were of great significance at his time and they had a strong impact on the work by others later in mathematics, proof theory, computer science, and artificial intelligence. Even today the name “Herbrand” can be found astonishingly often in research papers in fields that did not even exist at his time.^{2}

Let us start this introductory lecture by sketching a preliminary list of topics that were influenced by Herbrand’s work.

1Cf. [Vihan, 1995].

2To wit, the search in any online library (e.g. citeseer) reveals that astonishingly many authors dedicate parts of their work directly to Jacques Herbrand. A “Google Scholar” search gives a little less than ten thousand hits and the phrases we find by such an experiment include: Herbrand agent language, Herbrand analyses, Herbrand automata, Herbrand base, Herbrand complexity, Herbrand constraints, Herbrand disjunctions, Herbrand entailment, Herbrand equalities, Herbrand expansion, Herbrand’s Fundamental Theorem, Herbrand functions, Herbrand–Gentzen theorem, Herbrand interpretation, Herbrand–Kleene universe, Herbrand model, Herbrand normal forms, Herbrand procedures, Herbrand quotient, Herbrand realizations, Herbrand semantics, Herbrand strategies, Herbrand terms, Herbrand–Ribet theorem, Herbrand’s theorem, Herbrand theory, Herbrand universe. Whether and to what extend these references to Herbrand are justified is sometimes open for debate. This list shows, however, that in addition to the foundational importance of his work at the time, his insights still have an impact on research even at the present time. Herbrand’s name is therefore not only frequently mentioned among the most important mathematicians and logicians of the 20^{th} century but also among the pioneers of modern computer science and artificial intelligence.

1.1 Proof Theory

Dirk van Dalen (born 1932) begins his review on [Herbrand, 1971] as follows:

“Much of the logical activity in the first half of this century was inspired by Hilbert’s programme, which contained, besides fundamental reflections on the nature of mathematics, a number of clear-cut problems for technically gifted people. In particular the quest for so-called “consistency proofs” was taken up by quite a number of logicians. Among those, two men can be singled out for their imaginative approach to logic and mathematics: Jacques Herbrand and Gerhard Gentzen. Their contributions to this specific area of logic, called “proof theory” (Beweistheorie) following Hilbert, are so fundamental that one easily recognizes their stamp in modern proof theory.”^{3}

Dalen continues:

“When we realize that Herbrand’s activity in logic took place in just a few years, we cannot but recognize him as a giant of proof theory. He discovered an extremely powerful theorem and experimented with it in proof theory. It is fruitless to speculate on the possible course Herbrand would have chosen, had he not died prematurely; a consistency proof for full arithmetic would have been within his reach.”^{4}

The major thesis of [Anellis, 1991] is that, building on the Löwenheim–Skolem Theorem, it was Herbrand’s work in elaborating Hilbert’s concept of “being a proof” that gave rise to the development of the variety of first-order calculi in the 1930s, such as the ones of the Hilbert school, and such as Natural Deduction and Sequent calculi in [Gentzen, 1935].

As will be shown in § 11, Herbrand’s Fundamental Theorem has directly influenced Paul Bernays’ work on proof theory.

The main inspiration in the unwinding programme,^{5} which — to save the merits of proof theory — Georg Kreisel (born 1923) suggested as a replacement for Hilbert’s failed programme, is Herbrand’s Fundamental Theorem, especially for Kreisel’s notion of a recursive interpretation of a logic calculus in another one,^{6} such as given by Herbrand’s Fundamental Theorem for his first-order calculus in the sentential tautologies over the language enriched with Skolem functions.

Herbrand’s approach to consistency proofs, as we will sketch in §§ 15 and 16, has a semantical flavor and is inspired by Hilbert’s evaluation method of ε-substitution, whereas it avoids the dependence on Hilbert’s ε-calculus. The main idea (cf. § 16) is to replace the induction axiom by recursive functions of finitistic character. Herbrand’s approach is

[Kreisel, 1958, p. 155]

3Cf. [Dalen, 1974, p. 544].

4Cf. [Dalen, 1974, p. 548].

5Cf. [Kreisel, 1951; 1952; 1958; 1982], and do not miss the discussion in [Feferman, 1996]!

“To determine the constructive (recursive) content or the constructive equivalent of the non-

constructive concepts and theorems used in mathematics, particularly arithmetic and analysis.”

6Cf. [Kreisel, 1958, p. 160] and [Feferman, 1996, p. 259f.].

in contrast to the purely syntactical style of Gentzen^{7} and Schütte^{8} in which semantical interpretation plays no rôle.

So-called Herbrand-style consistency proofs follow Herbrand’s idea of constructing finite sub-models to imply consistency by Herbrand’s Fundamental Theorem. During the early 1970s, this technique was used by Thomas M. Scanlon Jr. (born 1940) in collaboration with Dreben and Goldfarb.^{9} These consistency proofs for arithmetic roughly follow Ackermann’s previous proof,^{10} but they apply Herbrand’s Fundamental Theorem in advance and consider Skolemized form instead of Hilbert’s ε-terms.^{11}

Gentzen’s and Herbrand’s insight on Cut and modus ponens elimination and the existence of normal form derivations with mid-sequents had a strong influence on William Craig’s work on interpolation.^{12} The impact of Craig’s Interpolation Theorem to various disciplines in turn has recently been discussed at the Interpolations Conference in Honor of William Craig in May 2007.^{13}

1.2 Recursive Functions and Gödel’s 2^{nd} Incompleteness Theorem

As will be discussed in detail in § 17, in his 1934 Princeton lectures, Gödel introduced the notion of (general) recursive functions and mentioned that this notion had been proposed to him in a letter from Herbrand, cf. § 2. This letter, however, seems to have had more influence on Gödel’s thinking, namely on the consequences of Gödel’s 2^{nd} incompleteness theorem:

“Nowhere in the correspondence does the issue of general computability arise. Herbrand’s discussion, in particular, is solely trying to explore the limits of consistency proofs that are imposed by the second theorem. Gödel’s response also focuses on that very topic. It seems that he subsequently developed a more critical perspective on the very character and generality of this theorem.”

[Sieg, 2005, p. 180]

Sieg [2005] argues that the letter of Herbrand to Gödel caused a change of Gödel’s perception of the impact of his own 2^{nd} incompleteness theorem on Hilbert’s programme: Initially Gödel did assert that it would not contradict Hilbert’s viewpoint. Influenced by Herbrand’s letter, however, he accepted the more critical opinion of Herbrand on this matter.

7Cf. [Gentzen, 1936; 1938; 1943].

8Cf. [Schütte, 1960].

9Cf. [Dreben & Denton, 1970], [Scanlon Jr., 1973], [Goldfarb & Scanlon Jr., 1974].

10Cf. [Ackermann, 1940].

11Contrary to the proofs of [Dreben & Denton, 1970] and [Ackermann, 1940], the proof of [Scanlon Jr., 1973], which is otherwise similar to the proof of [Dreben & Denton, 1970], admits the inclusion of induction axioms over any recursive well-ordering on the natural numbers:

By an application of Herbrand’s Fundamental Theorem, from a given derivation of an inconsistency, we can compute a positive natural number n such that Property C of order n holds. Therefore, in his analog of Hilbert’s and Ackermann’s ε-substitution method, Scanlon can effectively pick a minimal counterexample on the champ fini T_{n} from a given critical counterexample, even if this neither has a direct predecessor nor a finite initial segment.

This result was then further generalized in [Goldfarb & Scanlon Jr., 1974] to ω-consistency of arithmetic.

12Cf. [Craig, 1957a; Craig, 1957b].

13Cf. http://sophos.berkeley.edu/interpolations/.

“An odd prime p is called irregular if the class number of the field Q(μ_{p}) is divisible by p (μ_{p} being, as usual, the group of p-th roots of unity). According to Kummer’s criterion, p is irregular if and only if there exists an even integer k with 2 ≤ k ≤ p − 3 such that p divides (the numerator of) k-th Bernoulli number B_{k}, given by the expansion

\frac{t}{e^{t} − 1} + \frac{t}{2} − 1 = ∑_{n≥2} \frac{B_{n}}{n!} t^{n}.

The purpose of this paper is to strengthen Kummer’s criterion. Let A be the ideal class group of Q(μ_{p}), and let C be the F_{p}-vector space A/A^{p}. The Galois group Gal(\overline{Q}/Q) acts on C through its quotient Δ = Gal(Q(μ_{p})/Q). Since all characters of Δ with values in \overline{F}_{p}^{∗} are powers of the standard character

χ : Gal(\overline{Q}/Q) → Δ ˜ ⟶F_{p}^{∗}

giving the action of Gal(\overline{Q}/Q) on μ_{p}, the vector space C has a canonical decomposition

C = ⨁_{i mod (p−1)} C(χ^{i}),

where

C(χ^{i}) = {c ∈ C|σc = χ^{i}(σ) c for all σ ∈ Δ}.

(1.1) Main Theorem. Let k be even, 2 ≤ k ≤ p − 3. Then p|B_{k} if and only if C(χ^{1−k}) ≠ 0 In fact, the statement that C(χ^{1−k}) ≠ 0 implies p|B_{k} is well known [Herbrand, 1932b, Th. 3]”

[Ribet, 1976, Theorem 1.1, p. 151]

Figure 1: Herbrand–Ribet Theorem

1.3 Algebra and Ring Theory

In 1930–1931, within a few months, Herbrand wrote several papers on algebra and ring theory. During his visit to Germany he met and briefly worked on this topic with Noether, Hasse, and Artin; cf. § 2. He contributed several new theorems of his own and simplified proofs of results by Leopold Kronecker (1823–1891), Heinrich Weber (1842–1913), Teiji Takagi (1875–1960), Hilbert, and Artin, thereby generalizing some of these results. The Herbrand–Ribet Theorem is a result on the class number of certain number fields and it strengthens Kummer’s convergence criterion; cf. Figure 1.

Note that there is no direct connection between Herbrand’s work on logic and his work on algebra. Useful applications of proof theory to mathematics are very rare. Kreisel’s “unwinding” of Artin’s proof of Artin’s Theorem into a constructive proof seems to be one of the few exceptions.^{14}

1.4 A first résumé

Our following lectures will be more self-contained than this introductory lecture. But already on the basis of this first overview, we just have to admit that Jacques Herbrand’s merits are so outstanding that he has no chance to escape idolization. Actually, he has left a world heritage in logic in a very short time. But does this mean that we should treat him just as an icon?

On a more careful look, we will find out that this genius had his flaws, just as everybody of us made of this strange protoplasmic variant of matter, and that he has left some of them in his scientific writings. And he can teach us not only to be less afraid of logic than of mountaineering; he can also provide us with a surprising amount of insight that partly still lies to be rescued from contortion in praise and faulty quotations.

1.5 Still ten minutes to go

Inevitably, when all introductory words are said, we will feel the urge to point out to the young students that there are things beyond the latest developments of computer technology or the fabric of the Internet: eternal truths valid on planet Earth but in all those far away galaxies just as well.

And as there are still ten minutes to go till the end of the lecture, the students listen in surprise to the strange tale about the unknown flying objects from the far away, now visiting planet Earth and being welcomed by a party of human dignitaries from all strata of society. Not knowing what to make of all this, the little green visitors will ponder the state of evolution on this strange but beautiful planet: obviously life is there — but can it think?

The Earthlings seem to have flying machines, they are all connected planet-wide by communicators — but can they really think? Their gadgets and little pieces of machinery appear impressive — but is there a true civilization on planet Earth? How dangerous are

[Artin, 1927, p. 109, modernized orthography]

14With Artin’s Theorem we mean:

“Eine rationale Funktion F (x_{1}, x_{2}, ⋯, x_{n}) von n Veränderlichen heiße definit, wenn sie für

kein reelles Wertsystem der x_{i} negative Werte annimmt.” [Artin, 1927, p. 100]

“Satz 4: Es sei R ein reeller Zahlkörper, der sich nur auf eine Weise ordnen lässt, wie zum

Beispiel der Körper der rationalen Zahlen, oder der aller reellen algebraischen Zahlen oder

der aller reellen Zahlen.

Dann ist jede rationale definite Funktion von x_{1}, x_{2}, ⋯, x_{n} mit Koëffizienten aus R

Summe von Quadraten von rationalen Funktionen der x_{i} mit Koëffizienten aus R.”

Cf. [Delzell, 1996] for the unwinding of Artin’s proof of Artin’s Theorem.

Cf. [Feferman, 1996] for a discussion of the application of proof theory to mathematics in general.

they, these Earthlings made of a strange protoplasmic variant of matter?

And then cautiously looking through the electronic windows of their flying unknown objects, they notice that strange little bearded Earthling, being pushed into the back by the more powerful dignitaries, who holds up a sign post with

⊧ ≡ ⊢

written on it.

Blank faces, not knowing what to make of all this, the oldest and wisest scientist is slowly moved out through the e-door of the flying object, slowly being put down to the ground, and now the bearded Earthling is asked to come forward and the two begin that cosmic debate about syntax and semantics, proof theory and model theory, while the dignitaries stay stunned and silent.

And soon there is a sudden flash of recognition and a warm smile on that green and wrinkled old face, who has seen it all and now waves back to his fellow travelers who remained safely within the flying object: “Yes, they have minds — yes oh yes!”

And this is why the name “Jacques Herbrand” is finally written among others with a piece of chalk onto the blackboard — and now that the introductory lecture is coming to a close, we promise to tell in the following lectures, what this name stands for and what that young scientist found out when he was only 21 years old.

2 Herbrand’s Life

This brief résumé of Jacques Herbrand’s life focuses on his entourage and the people he met.^{15} He was born on Feb. 12, 1908, in Paris, France, where his father, Jacques Herbrand Sr., worked as a trader in antique paintings.^{16} He remained the only child of his parents, who were of Belgian origin. He died — 23 years old — in a mountaineering accident on July 27, 1931, in La Bérarde, Isère, France.

In 1925, only 17 years old, he was ranked first at the entrance examination to the prestigious École Normale Supérieure (ENS)^{17} in Paris — but he showed little interest for the standard courses at the Sorbonne, which he considered a waste of time.^{16} However, he closely followed the famous “Séminaire Hadamard” at the Collège de France, organized by Jacques Salomon Hadamard (1865–1963), from 1913 until 1933.^{18} That seminar attracted many students. At Herbrand’s time, among these students, prominent in their later lives, were:

name  lifetime  year of entering the ENS
André Weil  (1906–1998) 1922
Jean Dieudonné (1906–1992) 1924
Jacques Herbrand (1908–1931) 1925
Albert Lautman (1908–1944) 1926
Claude Chevalley (1909–1984) 1926

Weil, Dieudonné, and Chevalley would later be known among the eight founding members of the renowned Bourbaki group: the French mathematicians who published the book series on the formalization of mathematics, starting with [Bourbaki, 1939ff.].

Weil, Lautman, and Chevalley were Herbrand’s friends. Chevalley and Herbrand became particularly close friends^{19} and they worked together on algebra.^{20} Chevalley depicts Herbrand as an adventurous, passionate, and often perfectionistic personality who was not only interested in mathematics, but also in poetry and sports.^{16} In particular, he seemed to have liked extreme sportive challenges: mountaineering, hiking, and long distance swimming. His interest in philosophical issues and foundational problems of science was developed well beyond his age.

At that time, the ENS did not award a diploma, but the students had to prepare the agrégation, an examination necessary to be promoted to professeur agrégé,^{21} even though most students engaged into research. Herbrand passed the agrégation in 1928, again ranked first, and he prepared his doctoral thesis under the direction of Ernest Vessiot (1865–1952), who was the director of the ENS since 1927.^{22}

15More complete accounts of Herbrand’s life and personality can be found in [Chevalley, 1935; 1982], [Chevalley & Lautman, 1931], [Gödel, 1986ff., Vol. V, pp. 3–25]. All in all, very little is known about his personality and life.

16Cf. [Chevalley, 1982].

17Cf. http://www.ens.fr for the ENS in general and http://www.archicubes.ens.fr for the former students of the ENS.

18Cf. [Cartwright, 1965, p. 82], [Dieudonné, 1999, p. 107].

19Catherine Chevalley, the daughter of Claude Chevalley has written to Peter Roquette on Herbrand:

“he was maybe my father’s dearest friend” [Roquette, 2000, p. 36, Note 44].

20Cf. [Herbrand & Chevalley, 1931].

21This corresponds to a high-school teacher. The original rôle of the ENS was to educate students to become high-school teachers. Also Jean-Paul Sartre started his career like this.

Herbrand submitted his thesis [Herbrand, 1930], entitled Recherches sur la théorie de la démonstration, on April 14, 1929. It was approved for publication on June 20, 1929. In October that year he had to join the army for his military service which lasted for one year in those days. He finally defended his thesis on June 11, 1930.^{23}

After completing his military service in September 1930, awarded with a Rockefeller Scholarship, he spent the academic year 1930–1931 in Germany and planned to stay in Princeton^{24} for the year after. He visited the following mathematicians:

hosting scientist  lifetime  place  time of Herbrand’s stay ; John von Neumann Emil Artin Emmy Noether^{25} (1903–1957) (1898–1962) (1882–1935) Berlin Hamburg Göttingen \begin{matrix}\{ \\ \{ \\ \{ \end{matrix} middle of Oct. 1930 middle of May 1931 middle of June 1931 middle of July 1931^{26}

Herbrand discussed his ideas with Paul Bernays (1888–1977) in Berlin, and he met Paul Bernays, David Hilbert (1862–1943), and Richard Courant (1988–1972) later in Göttingen.^{27}

On April 7, 1931, Herbrand wrote a letter to Kurt Gödel (1906–1978), who answered with some delay on July 25, most probably too late for the letter to reach Herbrand before his early death two days later.^{28}

In other words, although Jacques Herbrand was still a relatively unknown young scientist, he was well connected to the best mathematicians and logicians of his time, particularly to those interested in the foundations of mathematics.

Herbrand met Helmut Hasse (1898–1979) at the Schiefkörper-Kongress (Feb. 26 – March 1, 1931) in Marburg, and he wrote several letters including plenty of mathematical ideas to Hasse afterwards.^{29} After exchanging several compassionate letters with Herbrand’s father,^{30} Hasse wrote Herbrand’s obituary which is printed as the foreword to Herbrand’s article on the consistency of arithmetic [Herbrand, 1932a].

22It is interesting to note that Ernest Vessiot and Jacques Salomon Hadamard where the two top-ranked students at the examination for the ENS in 1884.

23One reason for the late defense is that because of the minor rôle mathematical logic played at that time in France, Herbrand’s supervisor Ernest Vessiot had problems finding examiners for the thesis. The final committee consisted of Ernest Vessiot, Arnaud Denjoy (1884–1974) and Maurice René Fréchet (1878–1973).

24Cf. [Gödel, 1986ff., Vol. V, p. 3f.]. Cf. [Roquette, 2009] for the letters between Hasse, Herbrand, and Joseph H. M. Wedderburn (1882–1948) (Princeton) on Herbrand’s visit to Princeton.

25Herbrand had met Noether already very early in 1931 in Halle an der Saale. Cf. [Lemmermeyer & Roquette, 2006, p.106, Note 10].

26According to [Dubreil, 1983, p.73], Herbrand stayed in Göttingen until the beginning of July 1931.

In his report to the Rockefeller Foundation Herbrand wrote that his stay in Germany lasted from Oct. 20, 1930, until the end of July 1931, which is unlikely because he died on July 27, 1931, in France.

27That Herbrand met Bernays, Hilbert, and Courant in Göttingen is most likely, but we cannot document it. Hilbert was still lecturing regularly in 1931, cf. [Reid, 1970, p.199]. Courant wrote a letter to Herbrand’s father, cf. [Herbrand, 1971, p. 25, Note 1].

28Cf. [Gödel, 1986ff., Vol. V, pp. 3–25].

29Cf. [Roquette, 2007; 2009].

30Cf. [Hasse & Herbrand Sr., 1931].

3 Finitistic Classical First-Order Proof Theory

Herbrand’s work on logic falls into the area of what is called proof theory today. More specifically, he is concerned with the finitistic analysis of two-valued (i.e. classical), firstorder logic and its relationship to sentential, i.e. propositional logic.

Over the millenia, logic developed as proof theory. The key observation of the ancient Greek schools, first formulated by Aristotle of Stagira (384–322 B.C.), is that certain patterns of reasoning are valid irrespective of their actual denotation. From “all men are mortal” and “Socrates is a man” we can conclude that “Socrates is mortal”, irrespectively of Socrates’ most interesting personality and the contentious meaning of “being mortal” in this and other possible worlds. The discovery of those patterns of reasoning, called syllogisms, where meaningless symbols are used instead of everyday words, was the starting point of the known history of mathematical logic in the ancient world. For over two millenia, the development of these rules for drawing conclusions from given assumptions just on the basis of their syntactical form was the main subject of logic.

Model theory — on the other hand — the study of formal languages and their interpretation, became a respectable way of logical reasoning through the seminal works of Leopold Löwenheim (1878–1957) and Alfred Tarski (1901–1983). Accepting the actual infinite, model theory considers the set-theoretic semantical structures of a given language. With Tarski’s work, the relationship between these two areas of logic assumed overwhelming importance — as captured in our little anecdote of the introductory lecture (§ 1.5), where ‘⊧’ signifies model-theoretic validity and ‘⊢’ denotes proof-theoretic derivability.^{31}

Herbrand’s scientific work coincided with the maturation of modern logic, as marked inter alia by Gödel’s incompleteness theorems of 1930–1931.^{32} It was strongly influenced by the foundational crisis in mathematics as well. Russell’s Paradox was not only a personal calamity to Gottlob Frege (1848–1925),^{33} but it jeopardized the whole enterprise of set theory and thus the foundation of modern mathematics. From an epistemological point of view, maybe there was less reason for getting scared as it appeared at the time: As Wittgenstein (1889–1951) reasoned later,^{34} the detection of inconsistencies is an inevitable element of human learning, and many logicians today would be happy to live at such an interesting time of a raging^{35} foundational crisis.

31As we will discuss in § 14, Jacques Herbrand still had problems in telling ‘⊢’ and ‘⊧’ apart: For instance, he blamed Löwenheim for not showing consistency of first-order logic, which is a property related to Herbrand’s ‘⊢’, but not to Löwenheim’s ‘⊧’.

32Cf. [Gödel, 1931], [Rosser, 1936]. For an interesting discussion of the reception of the incompleteness theorems cf. [Dawson Jr., 1991].

33Cf. [Frege, 1893/1903, Vol. II].

34Cf. [Wittgenstein, 1939].

35This crisis has actually never been resolved in the sense that we would have a single set theory that suits all the needs of a working mathematician.

“Early twentieth century mathematicians used the expression ‘The Crisis in Foundations’.

This crisis had many causes and — despite the disappearance of the expression from contem-

porary speech — has never really been resolved. One of its many causes was the increasing

formalisation of mathematics, which brought with it the realisation that the paradox of the

liar could infect even mathematics itself. This appears most simply in the form of Russell’s

paradox, appropriately in the heart of set theory.” [Forster, 1997, p. 838]

The development of mathematics, however, more often than not attracts the intelligent young men looking for clarity and reliability in a puzzling world, threatened by social complexity. As David Hilbert put it:

“Und wo sonst soll Sicherheit und Wahrheit zu finden sein, wenn sogar das mathematische Denken versagt?”^{36}

“Es bildet ja gerade einen Hauptreiz bei der Beschäftigung mit einem mathematischen Problem, dass wir in uns den steten Zuruf hören: da ist ein Problem, suche die Lösung; du kannst sie durch reines Denken finden; denn in der Mathematik gibt es kein Ignorabimus.”^{37}

Furthermore, Hilbert did not want to surrender to the new “intuitionistic” movements of Luitzen Brouwer (1881–1966) and Hermann Weyl (1885–1955), who suggested a restructuring of mathematics with emphasis on the problems of existence and consistency rather than elegance, giving up many previous achievements, especially in analysis and in the set theory of Georg Cantor (1845–1918):^{38}

“Aus dem Paradies, das uns Cantor geschaffen, soll uns niemand vertreiben.”^{39}

Building on the works of Richard Dedekind (1831–1916), Charles S. Peirce (1839–1914), Ernst Schröder (1841–1902), Gottlob Frege (1848–1925), and Guiseppe Peano (1858– 1932), the celebrated three volumes of Principia Mathematica [Whitehead & Russell, 1910–1913] of Alfred North Whitehead (1861–1947) and Bertrand Russell (1872–1970) had provided evidence that — in principle — mathematical proofs could be reduced to logic, using only a few rules of inference and appropriate axioms.

The goals of Hilbert’s programme on the foundation of mathematics, however, extended well beyond this: His contention was that the reduction of mathematics to formal theories of logical calculi would be insufficient to resolve the foundational crisis of mathematics, neither would it protect against Russell’s Paradox and other inconsistencies in the future — unless the consistency of these theories could be shown formally by simple means.

Let us elaborate on what was meant by these “simple means”.

36Cf. [Hilbert, 1926, p.170].

“And where else are security and truth to be found, if even mathematical thinking fails?”

37Cf. [Hilbert, 1926, p.180, modernized orthography].

“After all, one of the things that attract us most when we apply ourselves to a mathematical

problem is precisely that within us we always hear the call: here is a problem, search for

the solution; you can find it by pure thought, for in mathematics there is no ignorabimus.”

[Heijenoort, 1971a, p. 384, translation by Stefan Bauer-Mengelberg] 38Cf. [Brouwer, 1925a; 1925b; 1926], [Weyl, 1921; 1928], [Cantor, 1932].

39Cf. [Hilbert, 1926, p.170].

“No one shall drive us from the paradise Cantor has created.”

Until he moved to Göttingen, Hilbert lived in Königsberg, and his view on mathematics in the 1920s was partly influenced by Kant’s Critique of pure reason.^{40} Mathematics as directly and intuitionally perceived by a mathematician is called contentual^{43} (inhaltlich) by Hilbert. According to [Hilbert, 1926], the notions and methods of contentual mathematics are partly abstracted from finite symbolic structures (such as explicitly and concretely given natural numbers, proofs, and algorithms) where we can effectively decide (in finitely many effective steps) whether a given object has a certain property or not. Beyond these aposterioristic abstractions from phenomena, contentual mathematics also has a synthetic^{44} aprioristic^{45} aspect, which depends neither on experience nor on deduction, and which cannot be reduced to logic, but which is transcendentally related to intuitive conceptions. Or, as Hilbert put it:

“Schon Kant hat gelehrt – und zwar bildet dies einen integrierenden Bestandteil seiner Lehre –, dass die Mathematik über einen unabhängig von aller Logik gesicherten Inhalt verfügt und daher nie und nimmer allein durch Logik begründet werden kann, weshalb auch die Bestrebungen von Frege und Dedekind scheitern mussten. Vielmehr ist als Vorbedingung für die Anwendung logischer Schlüsse und für die Betätigung logischer Operationen schon etwas in der Vorstellung gegeben: gewisse, außer-logische konkrete Objekte, die anschaulich als unmittelbares Erlebnis vor allem Denken da sind.”^{46}

40The transcendental philosophy of pure speculative^{41} reason is developed in the main work on epistemology, the Critique of pure reason [Kant, 1781; 1787], of Immanuël Kant (1724–1804), who spent most of his life in Königsberg and strongly influenced the education on Hilbert’s high school and university in Königsberg. The Critique of pure reason elaborates how little we can know about things independent of an observer (things in themselves, Dinge an sich selbst) in comparison to our conceptions, i.e. the representations of the things within our thinking (Erscheinungen und sinnliche Anschauungen, Vorstellungen). In what he compared^{42} to the Kopernikan revolution [Kant, 1787, p. XVI], Kant considered the conceptions gained in connection with sensual experience to be real and partly objectifiable, and accepted the things in themselves only as limits of our thinking, about which nothing can be known for certain.

41The term “pure (speculative) reason” is opposed to “(pure) practical reason”.

42Contrary to what is often written, Kant never wrote of “his Kopernikan revolution of philosophy”. 43The word “contentual” did not use to be part of the English language until recently. For instance, it is

not listed in the most complete Webster’s [Gove, 1993]. According to [Heijenoort, 1971a, p. viii], this neologism was especially introduced by Stefan Bauer-Mengelberg as a translation for the word “inhaltlich” in German texts on mathematics and logic, because there was no other way to reflect the special intentions of the Hilbert school when using this word. In January 2008, “contentual” got 6350 Google hits, 5600 of which, however, contain neither the word “Hilbert” nor the word “Bernays”. As these hits also include a pop song, “contentual” is likely to become an English word outside science in the nearer future. For a comparison, there were 4 million Google hits for “contentious”.

44“synthetic” is the opposite of “analytic” and means that a statement provides new information that cannot be deduced from a given knowledge base. Contrary to Kant’s opinion that all mathematical theorems are synthetic [Kant, 1787, p.14], (contentual) mathematics also has analytic sentences. In particular, Kant’s example 7 + 5 = 12 becomes analytic when we read it as s^{7}(0) + s^{5}(0) = s^{12}(0) and assume the non-necessary, synthetic, aprioristic axioms x + 0 = x and x + s(y) = s(x + y). Cf. [Frege, 1884, § 89].

45“a priori” is the opposite of “a posteriori” and means that a statement does not depend on any form of experience. For instance, all necessary [Kant, 1787, p. 3] and all analytic [Kant, 1787, p.11] statements are a priori. Finally, Kant additionally assumes that all aprioristic statements are necessary [Kant, 1787, p. 219], which seems to be wrong, cf. Note 44.

46Cf. [Hilbert, 1926, p.170f., modernized orthography].

“Kant already taught — and indeed it is part and parcel of his doctrine — that mathematics has at its disposal a content secured independently of all logic and hence can never be provided with a foundation by means of logic alone; that is why the efforts of Frege and Dedekind were

To refer to intellectual concepts which are not directly related to sensual perception or intuitive conceptions, both Kant and Hilbert use the word “ideal”. Ideal objects and methods in mathematics — as opposed to contentual ones — may involve the actual infinite; such as quantification, ε-binding, set theory, and non-terminating computations.

According to both [Kant, 1787] and [Hilbert, 1926], the only possible criteria for the acceptance of ideal notions are consistency and usefulness. Contrary to Kant,^{48} however, Hilbert is willing to accept useful ideal theories, provided that their consistency can be shown with contentual and intuitively clear methods — i.e. with “simple means”.

These “simple means” that may be admitted here must be, on the one hand, sufficiently expressive and powerful to show the consistency of arithmetic, but, on the other hand, simple, i.e. intuitively clear and contentually reliable. The notion of Hilbert’s finitism was born out of the conflict of these two goals.

Moreover, Hilbert expresses the hope that the new proof theory, primarily developed to show the consistency of ideal mathematics with contentual means, would also admit (possibly ideal, i.e. non-finitistic) proofs of completeness^{49} for certain mathematical theories. If this goal of Hilbert’s programme had been achieved, then ideal proofs would have been justified as convenient short-cuts for constructive, contentual, and intuitively clear proofs, so that — even under the threat of Russell’s Paradox and others — there would be no reason to give up the paradise of axiomatic mathematics and abstract set theory.

And these basic convictions of the Hilbert school constituted the most important influence on the young student of mathematics Jacques Herbrand.

As Gödel showed with his famous incompleteness theorems in 1930–1931,^{32} however, the consistency of any (reasonably conceivable) recursively enumerable mathematical theory that includes arithmetic excludes both its completeness and the existence of a finitistic consistency proof.

Nevertheless, the contributions of Wilhelm Ackermann (1896–1962), Bernays, Herbrand, and Gentzen within Hilbert’s programme gave proof theory a new meaning as a field in which proofs are the objects and their properties and constructive transformations are the field of mathematical study, just as in arithmetic the numbers are the objects and their properties and algorithms are the field of study.

[Kant, 1787, p. 310, modernized orthography]

bound to fail. Rather, as a condition for the use of logical inferences and the performance of

logical operations, something must already be given to our faculty of representation, certain

extra-logical concrete objects that are intuitively present as immediate conceptions prior to all

thought.” [Heijenoort, 1971a, p. 376, translation by Stefan Bauer-Mengelberg, modified^{47}]

47We have replaced “extralogical” with “extra-logical”, and — more importantly — “experience” with “conception”, for the following reason: Contrary to “Erfahrung” (experience), the German word “Erlebnis”

does not suggest an aposterioristic intention, which would contradict the obviously aprioristic intention of Hilbert’s sentence.

48Kant considers ideal notions to be problematic, because they transcend what he considers to be the area of objective reality; cf. Note 40. For notions that are consistent, useful, and ideal, Kant actually introduces the technical term problematic (problematisch):

“Ich nenne einen Begriff problematisch, der keinen Widerspruch enthält, der auch als eine

Begrenzung gegebener Begriffe mit anderen Erkenntnissen zusammenhängt, dessen objektive

Realität aber auf keine Weise erkannt werden kann.”

49A theory is complete if for any formula A without free variables (i.e. any closed formula in the given language) which is not part of this theory, its negation ¬A is part of this theory.

4 Herbrand’s Main Contributions to Logic and his Notion of Intuitionism

The essential works of Herbrand on logic are his PhD thesis [Herbrand, 1930] and the subsequent journal article [Herbrand, 1932a], both to be found in [Herbrand, 1971].^{50}

The main contribution is captured in what is called today Herbrand’s Fundamental Theorem. Sometimes it is simply called “Herbrand’s Theorem”, but the longer name is preferable as there are other important “Herbrand theorems”, such as the Herbrand–Ribet Theorem. Moreover, Herbrand himself calls it “Théorème fondamental”.

The subject of Herbrand’s Fundamental Theorem is the effective reduction of (the semidecision problem of) provability in first-order logic to provability in sentential logic.

Here we use the distinction well-known to Herbrand and his contemporaries between first-order logic (where quantifiers bind variables ranging over objects of the universe, i.e. of the domain of reasoning or discourse) and sentential logic without any quantifiers. Validity of a formula in sentential logic is effectively decidable, for instance with the truth-table method.

Although Herbrand spends Chapter 1 of his thesis on the subject, he actually “shows no interest for the sentential work” [Heijenoort, 1986c, p.120], and takes it for granted.

A. Contrary to Gentzen’s Hauptsatz [Gentzen, 1935], Herbrand’s Fundamental Theorem starts right with a single sentential tautology (cf. § 9). He treats this property as given and does not fix a concrete method for establishing it.

B. The way Herbrand presents his sentential logic in terms of ‘¬’ and ‘∨’ indicates that he is not concerned with intuitionistic logic as we understand the term today.^{51}

Contrary to Gentzen’s sequent calculus LK [Gentzen, 1935], in Herbrand’s calculi we do not find something like a sub-calculus LJ for intuitionistic logic. Moreover, there is no way to generalize Herbrand’s Fundamental Theorem to include intuitionistic logic: Contrary to the Cut elimination in Gentzen’s Hauptsatz, the elimination of modus ponens according to Herbrand’s Fundamental Theorem does not hold for intuitionistic logic.

“All the attempts to generalize Herbrand’s theorem in that direction have only led to partial and unhandy results (see [Heijenoort, 1971b]).”

[Heijenoort, 1986c, p.120f.] When Herbrand uses the term “intuitionism”, this typically should be understood as referring to something closer to the finitism of Hilbert than to the intuitionism of Brouwer.^{52} This ambiguous usage of the term “intuitionism” — centered around the partial rejection of the Law of the Excluded Middle, the actual infinite, as well as quantifiers and other binders — was common in the Hilbert school at Herbrand’s time.^{53} Herbrand’s view on what he calls “intuitionism” is best captured in the following quote:

50This book is still the best source on Herbrand’s writings today. It is not just an English translation of Herbrand’s complete works on logic (all of Herbrand’s work in logic was written in French, cf. [Herbrand, 1968]), but contains additional annotation, brief introductions, and extended notes by Jean van Heijenoort, Burton Dreben, and Warren Goldfarb. Besides minor translational corrections, possible addenda for future editions would be the original texts in French; Herbrand’s mathematical writings outside of logic; some remarks on the two corrections of Herbrand’s False Lemma by Gödel and Heijenoort, respectively, cf. §§ 11 and 12 below; and Herbrand’s correspondence. The correspondence with Gödel is published in [Gödel, 1986ff., Vol. V, pp. 14–25]. Herbrand’s letters to Hasse are still in private possession according to [Roquette, 2007]. The whereabouts of the rest of his correspondence is unknown.

51Cf. e.g. [Heyting, 1930a; 1971], [Gentzen, 1935].

“Nous entendons par raisonnement intuitionniste, un raisonnement qui satisfait aux conditions suivantes: on n’y considère jamais qu’un nombre fini déterminé d’objets et de fonctions; celles-ci sont bien définies, leur définition permettant de calculer leur valeur d’une manière univoque; on n’affirme jamais l’existence d’un objet sans donner le moyen de le construire; on n’y considère jamais l’ensemble de tous les objets x d’une collection infinie; et quand on dit qu’un raisonnement (ou un théorème) est vrai pour tous ces x, cela signifie que pour chaque x pris en particulier, il est possible de répéter le raisonnement général en question qui ne doit être considéré que comme le prototype de ces raisonnements particuliers.”^{54}

Contrary to today’s precise meaning of the term “intuitionistic logic”, the terms “intuitionism” and “finitism” denote slightly different concepts, which are related to the philosophical background, differ from person to person, and vary over times.^{55}

While Herbrand is not concerned with intuitionistic logic, he is a finitist with respect to the following two aspects:

1. Herbrand’s work is strictly contained within Hilbert’s finitistic programme and he puts ample emphasis on his finitistic standpoint and the finitistic character of his theorems.

52Gödel, however, expressed a different opinion in a letter to Heijenoort of Sept. 18, 1964: “In Note 3 of [Herbrand, 1932a] he does not require the enumerability of mathematical objects, and gives a definition which fits Brouwer’s intuitionism very well”

[Gödel, 1986ff., Vol. V, p. 319f.]

53Cf. e.g. [Herbrand, 1971, p. 283f.], [Tait, 2006, p. 82ff.]. 54Cf. [Herbrand, 1932a, p. 3, Note 3]. Without the comma after “intuitionniste”, but with an additional

comma after “question” also in: [Herbrand, 1968, p. 225, Note 3].

“By an intuitionistic argument we understand an argument satisfying the following conditions: in it we never consider anything but a given finite number of objects and of functions; these functions are well-defined, their definition allowing the computation of their value in a univocal way; we never state that an object exists without giving the means of constructing it; we never consider the totality of all the objects x of an infinite collection; and when we say that an argument (or a theorem) is true for all these x, we mean that, for each x taken by itself, it is possible to repeat the general argument in question, which should be considered to be merely the prototype of the particular arguments.”

[Herbrand, 1971, Note 5, p. 288f., translation by Heijenoort]

55Regarding intuitionism, besides Brouwer, Weyl, and Hilbert, we may count Leopold Kronecker (1823– 1891) and Henri Poincaré (1854–1912) among the ancestors, and have to mention Arend Heyting (1898– 1980) for his major differing view, cf. e.g. [Heyting, 1930a; 1930b; 1971]. Deeper discussions of Herbrand’s notion of “intuitionism” can be found in [Heijenoort, 1986c, pp. 113–118] and in [Tait, 2006, p. 82ff.]. Moreover, we briefly discuss it in Note 138. For more on finitism cf. e.g. [Parsons, 1998], [Tait, 1981], [Zach, 2001]. For more on Herbrand’s background in philosophy of mathematics, cf. [Chevalley, 1935], [Dubucs & Égré, 2006].

2. Herbrand does not accept any model-theoretic semantics unless the models are finite. In this respect, Herbrand is more finitistic than Hilbert, who demanded finitism only for consistency proofs.

“Herbrand’s negative view of set theory leads him to take, on certain questions, a stricter attitude than Hilbert and his collaborators. He is more royalist than the king. Hilbert’s metamathematics has as its main goal to establish the consistency of certain branches of mathematics and thus to justify them; there, one had to restrict himself to finitistic methods. But in logical investigations other than the consistency problem of mathematical theories the Hilbert school was ready to work with set-theoretic notions.”

[Heijenoort, 1986c, p.118]

5 The Context of Herbrand’s Work on Logic

Let us now have a look at what was known in Herbrand’s time and at the papers that influenced his work on logic.

Stanisław Zaremba (1863–1942) is mentioned in [Herbrand, 1928], where Herbrand cites Zaremba’s textbook on mathematical logic [Zaremba, 1926], which clearly influenced Herbrand’s notation.^{56}

Herbrand’s subject, first-order logic, became a field of special interest not least because of the seminal paper [Löwenheim, 1915], which singled out first-order logic in the Theory of Relatives developed by Peirce and Schröder.^{57} With this paper, first-order logic became an area of special interest, due to the surprising meta-mathematical properties of this logic, which was intended to be an especially useful tool with a restricted area of application.^{58}

As the presentation in [Löwenheim, 1915] is opaque, Thoralf Skolem (1887–1963) wrote five clarifying papers contributing to the substance of Löwenheim’s Satz 2, the now famous Löwenheim–Skolem Theorem [Skolem, 1920; 1923b; 1928; 1929; 1941]. From these papers, Herbrand cites [Löwenheim, 1915] and [Skolem, 1920], and the controversy pro and contra Herbrand’s reading of [Skolem, 1923b] and [Skolem, 1928] will be presented in § 14 below.

While Herbrand neither cites Peano nor even mentions Frege, the Principia Mathematica [Whitehead & Russell, 1910–1913] were influential at his time, and he was well aware of this. Herbrand cites all editions of the Principia and there are indications that he studied parts of it carefully.^{59} But Russell’s influence is comparatively minor compared to Hilbert’s, as, indeed, Herbrand was most interested in proving consistency, decidability, and completeness. Jean van Heijenoort (1912–1986) notes on Herbrand:

56Cf. Goldfarb’s Note to [Herbrand, 1928] on p. 32ff. in [Herbrand, 1971]. Zaremba was one of the leading Polish mathematicians in the 1920s. He had close connections to Paris, but we do not know whether Herbrand ever met him.

57For the heritage of Peirce cf. [Peirce, 1885], [Brady, 2000]; for that of Schröder cf. [Schröder, 1895], [Brady, 2000], [Peckhaus, 2004].

58Without set theory, first-order logic was too poor to serve as such a single universal logic as the ones for which Frege, Peano, and Russell had been searching; cf. [Heijenoort, 1986a]. For the suggestion of first-order logic as the basis for set theory, we should mention [Skolem, 1923b], which is sometimes cited as of the year 1922, and therefore easily confused with [Skolem, 1923a]. For the emergence of first-order logic as the basis for mathematics see [Moore, 1987].

59Herbrand seems to have studied ∗9 and ∗10 of [Whitehead & Russell, 1910–1913, Vol. I] carefully, leaving traces in Herbrand’s Property A and in Chapter 2 of Herbrand’s PhD thesis, cf. [Heijenoort, 1986c, pp. 102–106].

“The difficulties provoked by the Russell Paradox, stratification, ramification, the problems connected with the axiom of infinity or the axiom of reducibility, nothing of that seems to retain his attention. The reason for this attitude is that Herbrand does not share Russell’s conception concerning the relation between logic and mathematics, but had adopted Hilbert’s. In 1930 Herbrand indicates quite well where he sees the limits of Russell’s accomplishment: ‘So far we have only replaced ordinary language with another more convenient one, but this does not help us at all with respect to the problems regarding the principles of mathematics.’ [Herbrand, 1930a, p. 248; 1971, p. 208]. And the sentence that follows indicates the way to be followed: ‘Hilbert sought to resolve the questions which can be raised by applying himself to the study of collections of signs which are translations of propositions true in a determinate theory.’ ” [Heijenoort, 1986c, p.105].

As Herbrand’s major orientation was toward the Hilbert school, it is not surprising that the majority of his citations^{60} refer to mathematicians related either to the Hilbert school or to Göttingen, which was the Mecca of mathematicians until its intellectual and organizational destruction by the Nazis in 1933.

By the title of his thesis Recherches sur la théorie de la démonstration, Herbrand clearly commits himself to King Hilbert’s following, and being the first contributor to Hilbert’s finitistic programme in France, he was given the opportunity to write on Hilbert’s logic in a French review journal, and this paper [Herbrand, 1930a] is historically interesting because it captures Herbrand’s personal view of Hilbert’s finitistic programme.

6 A Genius with some Flaws

On the one hand, Herbrand was a creative mathematician whose ideas were truly outstanding, not only for his time. Besides logic, he also contributed to class-field theory and to the theory of algebraic number fields. Although this is not our subject here, we should keep in mind that Herbrand’s contributions to algebra are as important from a mathematical point of view and as numerous as his contributions to logic.^{61} Among the many statements about Herbrand’s abilities as a mathematician is Weil’s letter to Hasse in August 1931 where he writes that he would not need to tell him what a loss Herbrand’s death means especially for number theory.^{62} As Peter B. Andrews put it:

“Herbrand was by all accounts a brilliant mathematician.”

[Andrews, 2003, p.171].

60In his thesis [Herbrand, 1930], Herbrand cites [Ackermann, 1925], [Artin & Schreier, 1927], [Behmann, 1922], [Bernays, 1928], [Bernays & Schönfinkel, 1928], [Hilbert, 1922b; 1926; 1928], [Hilbert & Ackermann, 1928], and [Neumann, 1925; 1927; 1928]. Furthermore, Herbrand cites [Nicod, 1917] in [Herbrand, 1930], [Ackermann, 1928] in [Herbrand, 1931], and [Hilbert, 1931] and [Gödel, 1931] in [Herbrand, 1932a].

61Cf. [Herbrand, 1930b; 1931e; 1931f; 1932b; 1932c; 1932d; 1932e; 1932f; 1933; 1936] and [Herbrand & Chevalley, 1931], as well as [Dieudonné, 1982].

62Cf. [Lemmermeyer & Roquette, 2006, p.119, Note 6].

On the other hand, Herbrand neither had the education nor the supervision to present his results in proof theory with the technical rigor and standard, say, of the Hilbert school in the 1920s, let alone today’s emphasis on formal precision.^{63} Finitistic proof theory sometimes strictly demands the disambiguation of form and content and a higher degree of precision than most other mathematical fields. Moreover, the field was novel at Herbrand’s time and probably hardly anybody in France was able to advise Herbrand competently. Therefore, Herbrand, a génie créateur, as Heijenoort called him,^{64} was apt to make undetected errors. Well known today is a serious flaw in his thesis which stayed unnoticed by its reviewers at the time. Moreover, several theorems are in fact conceptually correct, but incorrectly formulated.

Let us have a look at three flaws in § 3.3 of the Chapters 2, 3 and 5, respectively:

Chapter 2, § 3.3: A typical instance for an incorrectly formulated theorem which is conceptually correct can be found in Chapter 2, § 3.3, on deep inference: From ⊢ B ⇒ C we can conclude ⊢ A[B] ⇒ A[C], provided that [⋯] denotes only positive positions^{65} in A. Herbrand, however, states

⊢ (B ⇒ C) ⇒ (A[B] ⇒ A[C])

which is not valid; to wit^{66} apply the substitution { A[…] ↦ ∀x. […], B ↦ true, C ↦ P(x) }.

Chapter 3, § 3.3: Incorrectly formulated is also Herbrand’s theorem on the relativization of quantifiers.^{67} This error was recognized later by Herbrand himself.^{68}

Moreover, notice that in this context, Herbrand discusses the many-sorted first-order logic related to the restriction to the language where all quantifiers are relativized, extending a similar discussion found already in [Peirce, 1885].

[Herbrand, 1971, p.V]

63Heijenoort writes in his well-known “source book”:

“Herbrand’s thesis bears the marks of hasty writing; this is especially true of Chapter 5. Some

sentences are poorly constructed, and the punctuation is haphazard. Herbrand’s thoughts are

not nebulous, but they are so hurriedly expressed that many a passage is ambiguous or

obscure. To bring out the proper meaning of the text the translators had to depart from a

literal rendering, and more rewriting has been allowed in this translation than in any other

translation included in the present volume.” [Heijenoort, 1971a, p. 525] Similarly, Warren Goldfarb, the translator and editor of Herbrand’s logical writings, writes:

“Herbrand also tended to express himself rather hastily, resulting in many obscurities; in these

translations an attempt has been made to balance the demands of literalness and clarity.”

64Cf. [Herbrand, 1968, p.1].

65Note that a position in a formula (seen as a tree built-up from logical operators ‘∧’, ‘∨’, ‘¬’, ‘∀’, and ‘∃’) is positive if the number of ¬-operators preceeding it on the path from the root position is even, and negative if it is uneven.

66Cf. also [Herbrand, 1971, Goldfarb’s Notes 6 (p.78) and A (p. 98)].

67Relativization of quantifiers was first discussed in the elaboration of first-order logic in [Peirce, 1885].

Roughly speaking, it means to restrict quantifiers to a predicate P by replacing any ∀x. A with ∀x. (P(x) ⇒ A), and, dually, ∃x. A with ∃x. (P(x) ∧ A).

68In Note 1 of [Herbrand, 1932a].

All of this is not terribly interesting, except that it gives us some clues on how Herbrand developed his theorems: It seems that he started, like any mathematician, with a strong intuition of the semantics and used it to formulate the theorem. Then he had a careful look at those parts of the proof that might violate the finitistic standpoint. The final critical check of minor details of the formalism in the actual proof,^{69} however, hardly played a rôle in this work.

Chapter 5, § 3.3: The drawback of his intuitive style of work manifests itself in a serious mistake, which concerns a lemma that has crucial applications in the proof of the Fundamental Theorem, namely the “lemma” of Chapter 5, § 3.3, which we will call Herbrand’s False Lemma. Before we discuss this in § 11, however, we have to define some notions.

7 Champs Finis, Herbrand Universe, and Herbrand Expansion

Most students of logic or computer science know Herbrand’s name in the form of Herbrand universe or Herbrand expansion. Today, the Herbrand universe is usually defined as the set of all terms over a given signature, and the Herbrand expansion of a set of formulas results from a systematic replacement of all variables in that set of formulas with terms from the Herbrand universe.

Historically, however, this is not quite correct. First of all, Herbrand does not use term structures for two reasons:

1. Herbrand typically equates terms with objects of the universe, and thereby avoids working explicitly with term structures.^{70}

2. As a finitist more royal than King Hilbert, Herbrand does not accept structures with infinite universes.

As a finite substitute for a typically infinite full term universe, Herbrand uses what he calls a champ fini of order n, which we will denote with T_{n}. Such a champ fini differs from a full term universe in containing only the terms t with |t| < n. We use |t| to denote the height of the term t, which is given by

|f(t_{1}, …, t_{m})| = 1 + max{0, |t_{1}| , …, |t_{m}| }.

The terms of T_{n} are constructed from the function symbols and constant symbols (which we will tacitly subsume under the function symbols in the following) of a finite signature and from a finite set of variables. We will assume that an additional variable l, the lexicon, is included in this construction, if necessary to have T_{n} ≠ ∅.

Herbrand prefers to treat all logical symbols besides ‘¬’, ‘∨’, and ‘∃’ as defined. Only in prenex forms, the universal quantifier ‘∀’ is also treated as a primitive symbol.

69Cf. [Hadamard, 1949, Chapter V] for a nice account of this mode of mathematical creativity.

70As this equating of terms has no essential function in Herbrand’s works, but only adds extra complication to Herbrand’s subjects, we will completely ignore it here and exclusively use free term structures in what follows.

The first elaborate description of first-order logic — under the name “first-intentional logic of relatives” — was published by Peirce [1885] shortly after the invention of quantifiers by Frege [1879]. What today we call an Herbrand expansion was implicitly given already in that publication [Peirce, 1885]. Herbrand spoke of “reduction” (réduite) instead.

Definition 7.1 (Herbrand Expansion, A^{T}) For a finite set of terms T , the expansion A^{T} of a formula A is defined as follows: A^{T} = A if A does not have a quantifier, (¬A)^{T} = ¬A^{T}, (A ∨ B)^{T} = A^{T} ∨ B^{T}, (∃x. A)^{T} = ⋁_{t∈T} A^{T}{x↦t}, and (∀x. A)^{T} = ⋀_{t∈T} A^{T}{x↦t}, where A^{T}{x↦t} denotes the result of applying the substitution {x↦t} to A^{T}. □

Example 7.2 (Herbrand Expansion, A^{T}) For example, for T := { 3, z + 2 }, and for A being the arithmetic formula

∀x. (x = 0 ∨ ∃y. x = y + 1),

the expansion A^{T} is

( \begin{matrix}& 3 = 0 \\ ∨ & 3 = 3 + 1 \\ ∨ & 3 = (z + 2) + 1 \end{matrix} ) ∧ ( \begin{matrix}& z + 2 = 0 \\ ∨ & z + 2 = 3 + 1 \\ ∨ & z + 2 = (z + 2) + 1 \end{matrix} ).

□

The Herbrand expansion reduces a first-order formula to sentential logic in such a way that a sentential formula is reduced to itself, and that the semantics is invariant if the terms in T range over the whole universe. If, however, this is not the case — such as in our above example and for all infinite universes —, then Herbrand expansion changes the semantics by relativization of the quantifiers^{67} to range only over those elements of the universe to which the elements of T evaluate.

8 Skolemization, Smullyan’s Uniform Notation, and γ- and δ-quantification

A first-order formula may contain existential as well as universal quantifiers. Can we make it more uniform by replacing either of them?

Consider the formula ∀x. ∃y. Q(x, y). These two quantifiers express a functional dependence between the values for x and y, which could also be expressed by a (new) function, say g, such that ∀x. Q(x, g(x)), i.e. this function g chooses for each x the correct value for y, provided that it exists. In other words, we can replace any existentially quantified variable x which occurs in the scope of universal quantifiers for y_{1}, …, y_{n} with the new Skolem term g(y_{1}, …, y_{n}).

This replacement, carried out for all existential quantifiers, results in a formula having only universal quantifiers. Using the convention that all free variables are universally quantified, we may then just drop these quantifiers as well. Roughly speaking, this transformation, Skolemization as we call it today, leaves satisfiability invariant. It occurs for the first time explicitly in [Skolem, 1928], but was already used in an awkward formulation in [Schröder, 1895] and [Löwenheim, 1915].

For reasons that will become apparent later, Herbrand employs a form of Skolemization that is dual to the one above. Now the universal variables are removed first, so that all remaining variables are existentially quantified. How can this be done? Well, if the universally quantified variable x occurs in the scope of the existentially quantified variables y_{1}, …, y_{m}, we can replace x with the Skolem term x^{δ}(y_{1}, …, y_{m}). The second-order variable or first-order function symbol x^{δ} in this Skolem term stands for any function with arguments y_{1}, …, y_{m}. Roughly speaking, this dual form of Skolemization leaves validity invariant.

For example, let us consider the formula ∃y. ∀x. Q(x, y). Assuming the Axiom of Choice and the standard interpretation of (higher-order) quantification, all of the following statements are logically equivalent:

• ∃y. ∀x. Q(x, y) holds.

• There is an object y such that Q(x, y) holds for every object x.

• ∃y. Q(x^{δ}(y), y) holds for every function x^{δ}.

• ∀f. ∃y. Q(f(y), y) holds.

Now ∃y. Q(x^{δ}(y), y) is called the (validity) Skolemized form of ∃y. ∀x. Q(x, y). The variable or function symbols x^{δ} of increased logical order are called Skolem functions.^{71} The Skolemized form is also called functional form (with several addenda specifying the dualities), because Skolemization turns the object variable x into a function variable or function symbol x^{δ}(⋯).

Note that A⇒B and ¬A ∨ B and ¬(A ∧ ¬B) are equivalent in two-valued logic. So are ¬∀x. A and ∃x. ¬A, as well as ¬∃x. A and ∀x. ¬A.

Accordingly, the uniform notation (as introduced in [Smullyan, 1968]) is a modern classification of formulas into only four categories: α, β, γ, and δ.

More important than the classification of formulas is the associated classification of the reductive inference rules applicable to them as principal formulas.

According to [Gentzen, 1935], but viewed under the aspect of reduction (i.e. the converse of deduction), the principal formula of an inference rule is the one which is (partly) replaced by its immediate “sub”-formulas, depending on its topmost operator.

• An α-formula is one whose validity reduces to the validity of a single operand of its topmost operator. For example, A ∨ B may be reduced either to A or to B, and A ⇒ B may be reduced either to ¬A or to B.

• A β-formula is one whose validity reduces to the validity of both operands of its topmost binary operator, introducing two cases of proof (β = \underline{b}ranching). For example, A ∧ B reduces to both A and B, and ¬(A ⇒ B) reduces to both A and ¬B.

71Herbrand calls Skolem functions index functions, translated according to [Herbrand, 1971]. Moreover, in [Dreben & Denton, 1970], [Scanlon Jr., 1973], and [Goldfarb & Scanlon Jr., 1974], we find the term indicial functions instead of “index functions”. The name “Skolem function” was used in [Gödel, 1939], probably for the first time, cf. [Anellis, 2006].

• A γ-formula is one whose validity reduces to the validity of alternative instances of its topmost quantifier. For example, ∃y. A reduces to A{y↦y^{γ}} in addition to ∃y. A, for a fresh free γ-variable y^{γ}. Similarly, ¬∀y. A reduces to ¬A{y↦y^{γ}} in addition to ¬∀y. A. Free γ-variables may be globally instantiated at any time in a reduction proof.

• A δ-formula is one whose validity reduces to the validity of the instance of its topmost quantifier with its Skolem term. For example, ∀x. A reduces to A{x↦x^{δ}(y1^{γ}, …, ym^{γ})}, where y1^{γ}, …, ym^{γ} are the free γ-variables already in use.^{72}

For a more elaborate introduction into free γ- and δ-variables see [Wirth, 2008].

Herbrand considers validity and Skolemized form as above in his thesis. In a similar context, which we will have to discuss below, Skolem considers unsatisfiability, a dual of validity, and Skolem normal form in addition to Skolemized form. As it was standard at his time, Herbrand called the two kinds of quantifiers — i.e. for γ- and δ-formulas^{73} — restricted and general quantifiers, respectively. To avoid the problem of getting lost in several dualities in what follows, we prefer to speak of γ-quantifiers and δ-quantifiers instead. The variables bound by δ-quantifiers will be called bound δ-variables. The variables bound by γ-quantifiers will be called bound γ-variables.

For a first-order formula A in which any bound variable is bound exactly once and does not occur again free, we define:

The outer^{74} Skolemized form of A results from A by removing any δ-quantifier and replacing its bound variable x with x^{δ}(y_{1}, …, y_{m}), where x^{δ} is a new symbol and y_{1}, …, y_{m}, in this order,^{75} are the variables of the γ-quantifiers in whose scope the δquantifier occurs.

72In the game-theoretic semantics of first-order logic, the δ-variables (such as x^{δ} in the above example) stand for the unknown choices by our opponent in the game, whereas, for showing validity, we have to specify a winning strategy by describing a finite number of first-order terms as alternative solutions for the γ-variables (such as yi^{γ} above), cf. e.g. [Hintikka, 1996].

73Notice that it is obvious how to generalize the definition of α-, β-, γ- and δ-formulas from top positions to inner occurrences according to the category into which they would fall in a stepwise reduction. Therefore, we can speak of α-, β-, γ- and δ-formulas also for the case of subformulas and classify their quantifiers accordingly.

74Herbrand has no name for the outer Skolemized form and he does not use the inner Skolemized form, which is the current standard in two-valued first-order logic and which is required for our discussion in Note 90. The inner Skolemized form of A results from A by repeating the following until all δ-quantifiers have been removed: Remove an outermost δ-quantifier and replace its bound variable x with x^{δ}(y_{1}, …, y_{m}), where x^{δ} is a new symbol and y_{1}, …, y_{m}, in this order, are the variables of the γ-quantifiers in whose scope the δ-quantifier occurs and which actually occur in the scope of the δ-quantifier. The inner Skolemized form is closely related to the liberalized δ-rule (also called δ^{+}-rule) in reductive calculi, such as sequent, tableau, or matrix calculi; cf. e.g. [Baaz & Fermüller, 1995], [Nonnengart, 1996], [Wirth, 2004, §§ 1.2.3 and 2.1.5], [Wirth, 2006], [Wirth, 2008, § 4].

75Contrary to our fixation of the order of the variables as arguments to the Skolem functions (to achieve uniqueness of the notion), Herbrand does not care for the order in his definition of the outer Skolemized form. Whenever he takes the order into account, however, he orders by occurrence from left to right or else by the height of the terms w.r.t. a substitution, but never by the names of the variables.

9 Axioms and Rules of Inference

In the following we will present the calculi of Herbrand’s thesis (i.e. the axioms and rules of inference) as required for our presentation of the Fundamental Theorem.

When we speak of a term, a formula, or a structure, we refer to first-order terminology without mentioning this explicitly. When we explicitly speak of “first order”, however, this is to emphasize the contrast to sentential logic.

Sentential Tautology: Let B be a first-order formula. B is a sentential tautology if it is quantifier-free and truth-functionally valid, provided its atomic subformulas are read as atomic sentential variables.^{76}

Modus Ponens: \frac{A A ⇒ B}{B}.

Generalized Rule of γ-Quantification: \frac{A[B\{x ↦ t\}]}{A[γx. B]}, where the free variables of the

term t must not be bound by quantifiers in B, and γ stands for ∃ if […] denotes a positive position^{65} in A[…], and γ stands for ∀ if this position is negative. Moreover, we require that […] does not occur in the scope of any quantifier in A[…]. This requirement is not necessary for soundness, but for the constructions in the proof of Herbrand’s Fundamental Theorem.

For example, we get

\frac{(t ≺ t) ∨ ¬(t ≺ t)}{(t ≺ t) ∨ ∃x. ¬(x ≺ t)}

and

\frac{(t ≺ t) ∨ ¬(t ≺ t)}{(t ≺ t) ∨ ¬∀x. (x ≺ t)}

via the meta-level substitutions

{ A[…] ↦ (t ≺ t) ∨ […], B ↦ ¬(x ≺ t) }

and

{ A[…] ↦ (t ≺ t) ∨ ¬[…], B ↦ (x ≺ t) },

respectively.

Note that Herbrand considers equality of formulas only up to renaming of bound variables and often implicitly assumes that a bound variable is bound only once and does not occur free. Thus, if a free variable y of the term t is bound by quantifiers in B, an implicit renaming of the bound occurrences of y in B is admitted to enable backward application of the inference rule.

76Notice that this notion is more restrictive than the following, which is only initially used by Herbrand in his thesis, but which is standard for the predicate calculi of the Hilbert school and the Principia Mathematica; cf. [Hilbert & Bernays, 1968/70, Vol. II, Supplement I D], [Whitehead & Russell, 1910–1913, *10].

B is a substitutional sentential tautology if there is a truth-functionally valid sentential formula A and a substitution σ mapping any sentential variable in A to a first-order formula such that B is Aσ. For example, both P(x) ∨ ¬P(x) and ∃x. P(x) ∨ ¬∃x. P(x) are substitutional sentential tautologies, related to the truth-functionally valid sentential formula p ∨ ¬p, but only the first one is a sentential tautology.

Generalized Rule of δ-Quantification: \frac{A[B]}{A[δx. B]}, where the variable x must not oc-

cur in the context A[…], and δ stands for ∀ if […] denotes a positive position in A[…], and δ stands for ∃ if this position is negative. Moreover, both for soundness and for the reason mentioned above, we require that […] does not occur in the scope of any quantifier in A[…]. Again, if x occurs in the context A[…], an implicit renaming of the bound occurrences of x in δx. B is admitted to enable backward application.

Generalized Rule of Simplification: \frac{A[B ∘ B]}{A[B]}, where ∘ stands for ∨ if […] denotes

a positive position in A[…], and ∘ stands for ∧ if this position is negative. To enable a forward application of the inference rule, the bound variables may be renamed such that the two occurrences of B become equal. Moreover, the Generalized Rule of γ-Simplification is the sub-rule for the case that B is of the form ∃y.C if […] denotes a positive position in A[…], and of the form ∀y.C if this position is negative.

To avoid the complication of quantifiers within a formula, where it is hard to keep track of the scope of each individual quantification, all quantifiers can be moved to the front, provided some caution is taken with the renaming of quantified variables. This is called the prenex form of a formula. The anti-prenex form results from the opposite transformation, i.e. from moving the quantifiers inwards as much as possible. Herbrand achieves these transformations with his Rules of Passage.

Rules of Passage: The following six logical equivalences may be used for rewriting from left to right (prenex direction) and from right to left (anti-prenex direction), resulting in twelve deep inference rules:

\begin{aligned}(1) & ¬∀x.A & ⇔ & ∃x.¬A \\ (2) & ¬∃x.A & ⇔ & ∀x.¬A \\ (3) & (∀x.A) ∨ B & ⇔ & ∀x. (A ∨B) \\ (4) & B ∨ ∀x.A & ⇔ & ∀x. (B ∨A) \\ (5) & (∃x.A) ∨ B & ⇔ & ∃x. (A ∨B) \\ (6) & B ∨ ∃x.A & ⇔ & ∃x. (B ∨A) \end{aligned}

Here, B is a formula in which the variable x does not occur. As explained above, if x occurs free in B, an implicit renaming of the bound occurrences of x in A is admitted to enable rewriting in prenex direction.

If we restrict the “Generalized” rules to outermost applications only (i.e., if we restrict A to be the empty context), we obtain the rules without the attribute “Generalized”, i.e. the Rules of γ- and δ-Quantification and the Rule of Simplification.^{77}

77The Generalized Rules of Quantification are introduced (under varying names) in [Heijenoort, 1968; 1975; 1982; 1986c] and under the names (μ^{∗}) and (ν^{∗}) in [Hilbert & Bernays, 1968/70, Vol. II, p.166], but only in the second edition of 1970, not in the first edition of 1939. Herbrand had only the nongeneralized versions of the Rules of Quantification and named them “First and Second Rule of Generalization”, translated according to [Herbrand, 1971]. Note that the restrictions of the Generalized Rules of Quantification guarantee the equivalence of the generalized and the non-generalized versions by the Rules of Passage; cf. [Heijenoort, 1968, p. 6]. Herbrand’s name for modus ponens is “Rule of Implication”.

Moreover, “(Generalized) Rule of Simplification” and “Rules of Passage” are Herbrand’s names. All other names introduced in § 9 are our own invention to simplify our following presentation.

10 Normal Identities, Properties A, B, and C, and Herbrand Disjunction and Complexity

Key notions of Herbrand’s thesis are normal identity, Property A, Property B, and Property C. Property C is the most important and the only one we need in this account.^{78}

Herbrand’s Property C was implicitly used already in [Löwenheim, 1915] and [Skolem, 1928], but as an explicit notion, it was first formulated in Herbrand’s thesis. It is the main property of Herbrand’s work and may well be called the central property of first-order logic, for reasons to be explained in the following.

In essence, Property C captures the following intuition taken from [Löwenheim, 1915]: Assuming the Axiom of Choice, the validity of a formula A is equivalent to the validity of its Skolemized form F. Moreover, the validity of F would be equivalent to the validity of the Herbrand expansion F^{U} for a universe U, provided only that this expansion were a finite formula and did not vary over different universes. To provide this, we replace the semantical objects of the universe U with syntactical objects, namely the countable set of all terms, used as “place holders” or names. To get a finite formula, we again replace this set of terms, which is infinite in general, with the champ fini T_{n}, as defined in § 7. If we can show F^{T_{n}} to be a sentential tautology for some positive natural number n, then we know that the γ-quantifications in F have solutions in any structure, so that F and A are valid.^{79} Otherwise, the Löwenheim–Skolem Theorem says that A is invalid.

Definition 10.1 (Property C, Herbrand Disjunction, Herbrand Complexity) Let A be a first-order formula, in which, without loss of generality, any bound variable is bound exactly once and does not occur again free, neither as a variable nor as a function symbol. Let F be the outer Skolemized form of A. Let n be a positive natural number. Let the champ fini T_{n} be formed over the function and free variable symbols occurring in F. A has Property C of order n if the Herbrand expansion F^{T_{n}} is a sentential tautology.

The Herbrand expansion F^{T_{n}} is sententially equivalent to the so-called Herbrand disjunction of A of order n, which is the finite disjunction ⋁_{σ:Y→T_{n}} Eσ, where Y is the set of bound (γ-) variables of F, and E results from F by removing all (γ-) quantifiers.

This form of representation can be used to define the Herbrand complexity of A, which is the minimal number of instances of E whose disjunction is a sentential tautology.^{80} □ Example 10.2 (Property C, Herbrand Disjunction, Herbrand Complexity) Let A be the following formula, which says that if we have transitivity and an upper bound of two elements, then we also have an upper bound of three elements:

78The following are the definitions for the omitted notions normal identity, Property A, and Property B for a formula D. D is a normal identity if D has a linear proof starting with a sentential tautology, possibly followed by applications of the Rules of Quantification, and finally possibly followed by applications of the Rules of Passage. D has Property A if D has a linear proof starting with a sentential tautology, possibly followed by applications of the Rules of Quantification, and finally possibly followed by applications of the Rules of Passage and the Generalized Rule of Simplification. Herbrand’s original definition of Property A is technically more complicated, but extensionally defines the same property and is also intensionally very similar. Finally, D has Property B of order n if D′ has Property C of order n, where D′ results from possibly repeated application of the Rules of Passage to D, in anti-prenex direction as long as possible.

79Indeed, we have F^{T_{n}} ⊢ A, cf. Theorem 4 in [Heijenoort, 1975], which roughly is our Lemma 13.1.

80Herbrand has no name for Herbrand disjunction and does not use the notion of Herbrand complexity, which, however, is closely related to Herbrand’s Fundamental Theorem, which says that the Herbrand complexity of A is always defined as a positive natural number, provided that ⊢A holds. More formally, the Herbrand complexity of A is defined as the minimal cardinality |S| such that, for some positive natural number m and some S ⊆ Y → T_{m}, the finite disjunction ⋁_{σ∈S} Eσ is a sentential tautology. It is useful in the comparison of logical calculi w.r.t. their smallest proofs for certain generic sets of formulas, cf. e.g. [Baaz & Fermüller, 1995].

\begin{matrix}& ∀a, b, c. (a ≺ b ∧ b ≺ c ⇒ a ≺ c) \\ ∧ & ∀x, y. ∃m. (x ≺ m ∧ y ≺ m) \\ ⇒ & ∀u, v, w. ∃n. (u ≺ n ∧ v ≺ n ∧ w ≺ n) \end{matrix} (A)

The outer Skolemized form F of A is

\begin{matrix}& ∀a, b, c. (a ≺ b ∧ b ≺ c ⇒ a ≺ c) \\ ∧ & ∀x, y. (x ≺ m^{δ}(x, y) ∧ y ≺ m^{δ}(x, y)) \\ ⇒ & ∃n. (u^{δ} ≺ n ∧ v^{δ} ≺ n ∧ w^{δ} ≺ n) \end{matrix} (F)

The result of removing the quantifiers from F is the formula E:

\begin{matrix}& (a ≺ b ∧ b ≺ c ⇒ a ≺ c) \\ ∧ & x ≺ m^{δ}(x, y) ∧ y ≺ m^{δ}(x, y) \\ ⇒ & u^{δ} ≺ n ∧ v^{δ} ≺ n ∧ w^{δ} ≺ n \end{matrix} (E)

By semantical considerations it is obvious that a solution for n is m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})). This is a term of height 3, which suggests that A has Property C of order 4. Let us show that this is indeed the case and that the Herbrand complexity of A is 2. Consider the following

2 substitutions: \begin{matrix}\{ & a & ↦ & v^{δ}, & b & ↦ & m^{δ}(v^{δ}, w^{δ}), & c & ↦ & m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})), \\ x & ↦ & v^{δ}, & y & ↦ & w^{δ}, & n & ↦ & m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) & \}; \\ \{ & a & ↦ & w^{δ}, & b & ↦ & m^{δ}(v^{δ}, w^{δ}), & c & ↦ & m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})), \\ x & ↦ & u^{δ}, & y & ↦ & m^{δ}(v^{δ}, w^{δ}), & n & ↦ & m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) & \}. \end{matrix}

Indeed, if we normalize the Herbrand disjunction generated by these two substitutions to a disjunctive normal form (i.e. a disjunctive set of conjunctions) we get the following sentential tautology.

\begin{aligned}\{ & v^{δ} ≺ m^{δ}(v^{δ}, w^{δ}) ∧ m^{δ}(v^{δ}, w^{δ}) ≺ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) ∧ v^{δ} ⊀ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})), \\ w^{δ} & ≺ & m^{δ}(v^{δ}, w^{δ}) & ∧ & m^{δ}(v^{δ}, w^{δ}) & ≺ & m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) & ∧ & w^{δ} & ⊀ & m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) & , \\ v^{δ} & ⊀ & m^{δ}(v^{δ}, w^{δ}) & , & w^{δ} & ⊀ & m^{δ}(v^{δ}, w^{δ}) & , \\ u^{δ} & ⊀ & m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) & , & m^{δ}(v^{δ}, w^{δ}) & ⊀ & m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) & , \\ & u^{δ} ≺ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) ∧ v^{δ} ≺ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) ∧ w^{δ} ≺ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) \} \end{aligned} (C)_{□}

The different treatment of δ-quantifiers and γ-quantifiers in Property C, namely by Skolemization and Herbrand expansion, respectively, as found in [Skolem, 1928] and [Herbrand, 1930], rendered the reduction to sentential logic by hand (or actually today, on a computer) practically executable for the first time.^{81} This different treatment of the two kinds of quantification is inherited from the Peirce–Schröder tradition^{57} which came on Herbrand via Löwenheim and Skolem. Russell and Hilbert had already merged that tradition with the one of Frege, sometimes emphasizing their Frege heritage over one of Peirce and Schröder.^{82} It was Herbrand who completed the bridge between these two traditions with his Fundamental Theorem, as depicted in § 12 below.

81For instance, the elimination of both γ- and δ-quantifiers with the help of Hilbert’s ε-operator suffers from an exponential complexity in formula size. As a result, already small formulas grow so large that the mere size makes them inaccessible to human inspection; and this is still the case for the term-sharing representation of ε-terms of [Wirth, 2008].

82While this emphasis on Frege will be understood by everybody who ever had the fascinating experience of reading Frege, it put some unjustified bias to the historiography of modern logic, still present in the selection of the famous source book [Heijenoort, 1971a]; cf. e.g. [Anellis, 1992, Chapter 3].

11 Herbrand’s False Lemma

For a given positive natural number n, Herbrand’s (False) Lemma says that Property C of order n is invariant under the application of the Rules of Passage.

The basic function of Herbrand’s False Lemma in the proof of Herbrand’s Fundamental Theorem is to establish the logical equivalence of Property C of a formula A with Property C of the prenex and anti-prenex forms of A, cf. § 9.

Herbrand’s Lemma is wrong because the Rules of Passage may change the outer Skolemized form. This happens whenever a γ-quantifier binding x is moved over a binary operator whose unchanged operand B contains a δ-quantifier.^{83}

To find a counterexample for Herbrand’s Lemma for the case of Property C of order 2, let us consider moving out the γ-quantifier “∃x.” in the valid formula

(∃x. P(x)) ∨ ¬∃y. P(y).

The (outer) Skolemized form of this formula is

(∃x. P(x)) ∨ ¬P(y^{δ}).

The Herbrand disjunction over the single substitution {x↦y^{δ}} is a sentential tautology. The outer Skolemized form after moving out the “∃x.” is

∃x. ( P(x) ∨ ¬P(y^{δ}(x)) ).

To get a sentential tautology again, we now have to take the Herbrand disjunction over both {x↦y^{δ}(l)} and {x↦l} (instead of the single {x↦y^{δ}}), for the lexicon l.

This, however, is not really a counterexample for Herbrand’s Lemma because Herbrand treated the lexicon l as a variable and defined the height of a Skolem constant to be 1, and the height of a variable to be 0, so that |y^{δ}| = 1 = |y^{δ}(l)|. As free variables and Skolem constants play exactly the same rôle, this definition of height is a bit unintuitive and was possibly introduced to avoid this counterexample. But now for the similar formula

( (∃x. P(x)) ∧ ∀y. Q(y) ) ∨ ¬(∃x. P(x)) ∨ ¬∀y. Q(y)

after moving the first γ-quantifier “∃x.” out over the “∧”, we have to apply

instead of \begin{matrix}\{ x ↦ x^{δ}, & y ↦ y^{δ}(x^{δ}) \} \\ \{ x ↦ x^{δ}, & y ↦ y^{δ} \} \end{matrix}

to get a sentential tautology, and we have |y^{δ}| = 1 and |y^{δ}(x^{δ})| = 2, and thus y^{δ} ∈ T_{2}, but y^{δ}(x^{δ}) ∉ T_{2}. This means: Property C of order 2 varies under a single application of a Rule of Passage, and thus we have a proper counterexample for Herbrand’s False Lemma here.

In 1939, Bernays remarked that Herbrand’s proof is hard to follow^{84} and — for the first time — published a sound proof of a version of Herbrand’s Fundamental Theorem which is restricted to prenex form, but more efficient in the number of terms that have to be considered in a Herbrand disjunction than Herbrand’s quite global limitation to all terms t with |t| < n, related to Property C of order n.^{85}

According to a conversation with Heijenoort in autumn 1963,^{86} Gödel noticed the lacuna in the proof of Herbrand’s False Lemma in 1943 and wrote a private note, but did not publish it. While Gödel’s documented attempts to construct a counterexample to Herbrand’s False Lemma failed, he had actually worked out a correction of Herbrand’s False Lemma, which is sufficient for the proof of Herbrand’s Fundamental Theorem.^{87}

83Here we use the same meta variables as in our description of the Rules of Passage in § 9 and assume that x does not occur free in B.

84In [Hilbert & Bernays, 1968/70, Vol. II], in Note 1 on p.158 of the 1939 edition (p.161 of the 1970 edition), we read: “Die Herbrandsche Beweisführung ist schwer zu verfolgen”

85Cf. § 3.3 of the 1939 edition of [Hilbert & Bernays, 1968/70, Vol. II]. In the 1970 edition, Bernays also indicates how to remove the restriction to prenex formulas.

86Cf. [Herbrand, 1968, p. 8, Note j].

In 1962, when Gödel’s correction was still unknown, a young student, Peter B. Andrews, had the audacity to tell his advisor Alonzo Church (1903–1995) that there seemed to be a gap in the proof of Herbrand’s False Lemma. Church sent Andrews to Burton Dreben (1927–1999), who finally came up with a counterexample. And then Andrews constructed a simpler counterexample (essentially the one we presented above) and joint work found a correction similar to Gödel’s,^{88} which we will call Gödel’s and Dreben’s correction in § 13.

Roughly speaking, the corrected lemma says that — to keep Property C of A invariant under (a single application of) a Rule of Passage — we may have to step from order n to order n (N^{r}+1)^{n}. Here r is the number of γ-quantifiers in whose scope the Rule of Passage is applied and N is the cardinality of T_{n} for the function symbols in the outer Skolemized form of A.^{89} This correction is not particularly elegant because — iterated several times until a prenex form is reached — it can lead to pretty high orders. Thus, although this correction serves well for soundness and finitism, it results in a complexity that is unacceptable in practice (e.g. in automated reasoning) already for small non-prenex formulas.

The problems with Herbrand’s False Lemma in the step from Property C to a proof without modus ponens in his Fundamental Theorem (cf. § 13) result primarily^{90} from a detour over prenex form, which was standard at Herbrand’s time. Löwenheim and Skolem had always reduced their problems to prenex forms of various kinds. The reduction of a proof task to prenex form has several disadvantages, however, such as serious negative effects on proof complexity.^{91} If Jacques Herbrand had known of his flaw, he would probably have avoided the whole detour over prenex forms, namely in the form of what we will call Heijenoort’s correction,^{92} which avoids an intractable and unintuitive^{93} rise in complexity, cf. § 13.

87Cf. [Goldfarb, 1993].

88Cf. [Andrews, 2003], [Dreben &al., 1963], [Dreben & Denton, 1963].

89Cf. [Dreben & Denton, 1963, p. 393].

90Secondarily, the flaw in Herbrand’s False Lemma is a peculiarity of the outer Skolemized form. For the inner Skolemized form (cf. Note 74), moving γ-quantifiers with the Rules of Passage cannot change the number of arguments of the Skolem functions. This does not help, however, because, for the inner Skolemized form, moving a δ-quantifier may change the number of arguments of its Skolem function if the Rule of Passage is applied within the scope of a γ-quantifier whose bound variable occurs in B but not

in A.^{83} The inner Skolemized form of ∃y_{1}. ∀z_{1}. Q(y_{1}, z_{1}) ∨ ∃y_{2}. ∀z_{2}. Q(y_{2}, z_{2}) is ∃y_{1}. Q(y_{1}, z1^{δ}(y_{1})) ∨ ∃y_{2}.

Q(y_{2}, z2^{δ}(y_{2})), but the inner Skolemized form of any prenex form has a binary Skolem function, unless we use Henkin quantifiers as found in Hintikka’s first-order logic, cf. [Hintikka, 1996].

91Cf. e.g. [Baaz & Fermüller, 1995]; [Baaz & Leitsch, 1995].

92The first published hints on Heijenoort’s correction are [Heijenoort, 1971a, Note 77, p. 555] and [Herbrand, 1971, Note 60, p.171]. On page 99 of [Heijenoort, 1986c], without giving a definition, Heijenoort speaks of generalized versions (which Herbrand did not have) of the rules of “existentialization and universalization”, which we have formalized in our Generalized Rules of Quantification in § 9. Having studied Herbrand’s PhD thesis [Herbrand, 1930] and [Heijenoort, 1968; 1975], what Heijenoort’s generalized rules must look like can be inferred from the following two facts: Herbrand has a generalized version of his Rule of Simplification in addition to a non-generalized one. Rewriting with the Generalized Rule of γ-Quantification within the scope of quantifiers would not permit Herbrand’s constructive proof of his Fundamental Theorem.

Note that Heijenoort’s correction avoids the detour over the Extended First ε-Theorem of the proof of Bernays mentioned above; cf. Note 85. Moreover, Heijenoort gets along without Herbrand’s complicated prenex forms with raised γ-multiplicity, which are required for Herbrand’s definition of Property A.

Notice, however, that Gödel’s and Dreben’s correction is still needed for the step from a proof with modus ponens to Property C, i.e. from Statement 4 to Statement 1 in Theorem 12.1. As the example on top of page 201 in [Herbrand, 1971] shows, an intractable increase of the order of Property C cannot be avoided in general for an inference step by modus ponens.

93Unintuitive e.g. in the sense of [Tait, 2006].

12 The Fundamental Theorem

The Fundamental Theorem of Jacques Herbrand is not easy to comprehend at first, because of its technical nature, but it rests upon a basic intuitive idea, which turned out to be one of the most profound insights in the history of logic.

We know — and so did Herbrand — that sentential logic is decidable: for any given sentential formula, we could, for instance, use truth-tables to decide its validity. But what about a first-order formula with quantifiers?

There is Löwenheim’s and Skolem’s observation that ∀x. P(x) in the context of the existentially quantified variables y_{1}, …, y_{n} stands for P(x^{δ}(y_{1}, …, y_{n})) for an arbitrary Skolem function x^{δ}(⋯), as outlined in § 8. This gives us a formula with existential quantifiers only. Now, taking the Herbrand disjunction, an existentially quantified formula can be shown to be valid, if we find a finite set of names denoting elements from the domain to be substituted for the existentially quantified variables, such that the resulting sentential formula is truth-functionally valid. Thus, we have a model-theoretic argumentation how to reduce a given first-order formula to a sentential one. The semantical elaboration of this idea is due to Löwenheim and Skolem, and this was known to Herbrand.

But what about the reducibility of an actual proof of a given formula within a first-order calculus?

The affirmative answer to this question is the essence of Herbrand’s Fundamental Theorem and the technical device, by which we can eliminate a switch of quantifiers (such as ∃y. ∀x. Q(x, y) of § 8) is captured in his Property C.

Thus, if we want to cross the river that divides the land of valid first-order formulas from the land of provable ones, it is the sentential Property C that stands firm in the middle of that river and holds the bridge, whose first half was built by Löwenheim and Skolem and the other by Herbrand:

Herbrand’s Fundamental Theorem shows that if a formula A has Property C of some order n — i.e., by the Löwenheim–Skolem Theorem, if A is a valid (⊧ A) — then we not only know of the existence of a proof in any of the standard proof calculi (⊢A), but we can actually construct a proof for A in Herbrand’s calculus from a given n. The proof construction process is guided by the champ fini of order n, whose size determines the multiplicities of γ-quantifiers and whose elements are the terms substituted as witnesses in the γ-Quantification steps. That proof begins with a sentential tautology and may use the Rules of γ- and δ-Quantification, the Generalized Rule of Simplification, and the Rules of Passage.

Contrary to what Herbrand’s False Lemma implies, a detour over a prenex form of A dramatically increases the order of Property C and thus the length of that proof, cf. § 11. Heijenoort, however, observed that this rise of proof length can be overcome by avoiding the problematic Rules of Passage with the help of deep (or Generalized) quantification rules, which may introduce quantifiers deep within formulas (“Heijenoort’s correction”). We have included these considerations into our statement of Herbrand’s Fundamental Theorem.

Theorem 12.1 (Herbrand’s Fundamental Theorem) Let A be a first-order formula in which each bound variable is bound by a single quantifier and does not occur free. The following five statements are logically equivalent. Moreover, we can construct a witness for any statement from a witness of any other statement.

1. A has Property C of order n for some positive natural number n.

2. We can derive A from a sentential tautology, starting possibly with applications of the Generalized Rules of γ- and δ-Quantification, which are then possibly followed by applications of the Generalized Rule of γ-Simplification.

3. We can derive A from a sentential tautology, starting possibly with applications of the Rules of γ- and δ-Quantification, which are then possibly followed by applications of the Generalized Rule of γ-Simplification and the Rules of Passage.

4. We can derive A from a sentential tautology with the Rules of γ- and δ-Quantification, the Rule of Simplification, the Rules of Passage, and Modus Ponens.

5. We can derive A in one of the standard first-order calculi of Principia Mathematica or of the Hilbert school.^{94} □

The following deserves emphasis: The derivations in the above Statements 2 to 5 as well as the number n of Statement 1 can be constructed from each other; and this construction is finitistic in the spirit of Herbrand’s basic beliefs in the nature of proof theory and meta-mathematics. Statement 2 is due to Heijenoort’s correction; cf. §§ 11 and 13. Statement 3 and Herbrand’s Property A are extensionally equal and intensionally very close to each other.

94Cf. [Whitehead & Russell, 1910–1913, *10], [Hilbert & Bernays, 1968/70, Vol. II, Supplement I D], respectively.

13 Modus Ponens Elimination

The following lemma provides the step from Statement 1 to Statement 2 of Theorem 12.1 with additional details exhibiting an elimination of modus ponens similar to the Cut elimination in Gentzen’s Hauptsatz.

We present the lemma in parallel both in the version of Gödel’s and Dreben’s correction and of Heijenoort’s correction.^{95} To melt these two versions into one, we underline the parts that are just part of Heijenoort’s correction and overline the parts that result from Gödel’s and Dreben’s. Thus, the lemma stays valid if we omit either the underlined or else the overlined part of it, but not both.

Lemma 13.1 (Modus Ponens Elimination)

Let A be a first-order formula \overline{in prenex form} in which each bound variable is bound by a single quantifier and does not occur free. Let F be the outer Skolemized form of A. Let Y be the set of bound (γ-) variables of F. Let E result from F by removing all (γ-) quantifiers. Let n be a positive natural number. Let the champ fini T_{n} be formed over the function and free variable symbols occurring in F. If A has Property C of order n, then we can construct a derivation of A of the following form, in which we read any term starting with a Skolem function as an atomic variable:

Step 1:

We start with \underline{a sentential tautology whose disjunctive normal form is a} \underline{re-ordering of a disjunctive normal form of} the sentential tautology ⋁_{σ:Y→T_{n}} Eσ.

Step 2: Then we may repeatedly apply the \underline{Generalized} Rules of γ- and δ-Quantification.

Step 3:

Then, (after renaming all bound δ-variables) we may repeatedly apply the Generalized Rule of γ-Simplification.

□

Obviously, there is no use of modus ponens in such a proof, and thus, it is linear, i.e. written as a tree, it has no branching. Moreover, all function and predicate symbols within this proof occur already in A, and all formulas in the proof are similar to A in the sense that they have the so-called “sub”-formula property.

Example 13.2 (Modus Ponens Elimination) (continuing Example 10.2) Let us derive the formula A of Example 10.2 in § 10. As A is not in prenex form we have to apply the version of Lemma 13.1 without the overlined part. As explained in Example 10.2, A has Property C of order n for n = 4, and the result of removing the quantifiers from the outer Skolemized form of A is the formula E:

\begin{matrix}& (a ≺ b ∧ b ≺ c ⇒ a ≺ c) \\ ∧ & x ≺ m^{δ}(x, y) ∧ y ≺ m^{δ}(x, y) \\ ⇒ & u^{δ} ≺ n ∧ v^{δ} ≺ n ∧ w^{δ} ≺ n \end{matrix} (E)

95Cf. § 11. We present Heijenoort’s correction actually in form of Theorem 4 in [Heijenoort, 1975] with a slight change, which becomes necessary for our use of Herbrand disjunction instead of the Herbrand expansion, namely the addition of the underlined part of Step 1 in Lemma 13.1.

Let N denote the cardinality of T_{n}. Let T_{n} = {t_{1}, …, t_{N}}.

For the case of n = 4, we have N = 3+3^{2}+(3 + 3^{2})^{2} = 156, and, for Y := {a, b, c, n, x, y}, the Herbrand disjunction ⋁_{σ:Y→T_{4}} Eσ has N^{|Y |} elements, i.e. more than 10^{13}. Thus, we had better try a reduction proof here,^{96} applying the inference rules backwards, and be content with arriving at a sentential tautology which is a sub-disjunction of a re-ordering of a disjunctive normal form of ⋁_{σ:Y→T_{4}} Eσ.

As the backwards application of the Generalized Rule of γ-Quantification admits only a single (i.e. linear) application of each γ-quantifier (or each “lemma”), and as we will have to apply both the first and the second line of A twice, we first increase the γ-multiplicity of the top γ-quantifiers of these two lines to two. This is achieved by applying the Generalized Rule of γ-Simplification twice backwards to A, resulting in:^{97}

∀a, b, c. (a ≺ b ∧ b ≺ c ⇒ a ≺ c)

∧ ∀a, b, c. (a ≺ b ∧ b ≺ c ⇒ a ≺ c)
∧ ∀x, y. ∃m. \binom{x ≺ m}{∧ y ≺ m}
∧ ∀x, y. ∃m. \binom{x ≺ m}{∧ y ≺ m}
⇒ ∀u, v, w. ∃n. (u ≺ n ∧ v ≺ n ∧ w ≺ n)

Renaming the bound δ-variables to some terms from T_{n}, and applying the Generalized Rule of δ-Quantification three times backwards in the last line, we get:

∀a, b, c. (a ≺ b ∧ b ≺ c ⇒ a ≺ c)

∧ ∀a, b, c. (a ≺ b ∧ b ≺ c ⇒ a ≺ c)
∧ ∀x, y. ∃ m^{δ}(v^{δ}, w^{δ}) . \binom{x ≺ m^{δ}(v^{δ}, w^{δ})}{∧ y ≺ m^{δ}(v^{δ}, w^{δ})}

∧ ∀x, y. ∃ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) . \binom{x ≺ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ}))}{∧ y ≺ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ}))}
⇒ ∃n. ( u^{δ} ≺ n ∧ v^{δ} ≺ n ∧ w^{δ} ≺ n)

The boxes indicate that the enclosed term actually denotes an atomic variable whose structure cannot be changed by a substitution. By this nice trick of taking outermost Skolem terms as names for variables, Herbrand avoids the hard task of giving semantics to Skolem functions, cf. § 14.^{98} We apply the Generalized Rule of γ-Quantification four times backwards, resulting in application of

96As Herbrand’s proof of his version of Lemma 13.1 [Herbrand, 1971, p.170] proceeds reductively too, we explain Herbrand’s general proof in parallel to the development of our special example, in Notes 97–99.

Herbrand’s proof is interesting by itself and similar to the later proof of the Second ε-Theorem in [Hilbert & Bernays, 1968/70, Vol. II, § 3.1].

97To arrive at the full Herbrand disjunction ⋁_{σ:Y→T_{n}} Eσ, Herbrand’s proof requires us to apply the Rule of Simplification top-down at each occurrence of a γ-quantifier N times, and the idea is to substitute t_{i} for the i^{th} occurrence of this γ-quantifier on each branch.

98According to Herbrand’s proof we would have to replace any bound δ-variable x with its Skolem term x^{δ}(t_{i_{0}}, …, t_{i_{k}}), provided that i_{0}, …, i_{k} denotes the branch on which this δ-quantifier occurs w.r.t. the previous step of raising each γ-multiplicity to N, described in Note 97.

{x ↦ v^{δ} , y ↦ w^{δ} }

to the third line and

{x ↦ u^{δ} , y ↦ m^{δ}(v^{δ}, w^{δ}) }

to the fourth line. This yields:^{99}

∀a, b, c. (a ≺ b ∧ b ≺ c ⇒ a ≺ c)
∧ ∀a, b, c. (a ≺ b ∧ b ≺ c ⇒ a ≺ c)
∧ ∃ m^{δ}(v^{δ}, w^{δ}) . ( v^{δ} ≺ m^{δ}(v^{δ}, w^{δ}) ∧ w^{δ} ≺ m^{δ}(v^{δ}, w^{δ}) )
∧ ∃ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ})) . \binom{u^{δ} ≺ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ}))}{∧ m^{δ}(v^{δ}, w^{δ}) ≺ m^{δ}(u^{δ}, m^{δ}(v^{δ}, w^{δ}))}
⇒ ∃n. ( u^{δ} ≺ n ∧ v^{δ} ≺ n ∧ w^{δ} ≺ n)

Applying (always backwards) the Generalized Rule of δ-Quantification twice and the Generalized Rule of γ-Quantification seven times, and then dropping the boxes (as they are irrelevant for sentential reasoning without substitution) and rewriting it all into a disjunctive list of conjunctions, we arrive at the disjunctive set C of Example 10.2, which is a sentential tautology. Moreover, as a list, C is obviously a re-ordered sublist of a disjunctive normal form of ⋁_{σ:Y→T_{4}} Eσ. □

In the time before Herbrand’s Fundamental Theorem, a calculus was basically a means to describe a set of theorems in a semi-decidable and theoretical fashion. In Hilbert’s calculi, for instance, the search for concrete proofs is very hard. Contrary to most other Hilbertstyle calculi, the normal form of proofs given in Statement 2 of Theorem 12.1, however, supports the search for reductive proofs: Methods of human^{100} and automatic^{101} proof search may help us to find simple proofs in this normal form.

This means that, for the first time in known history, Herbrand’s version of Lemma 13.1 gives us the means to search successfully for simple proofs in a formal calculus by hand (or actually today, on a computer), just as we have done in Example 13.2.^{102}

99Note that the terms to be substituted for a bound γ-variable, say y, in such a reduction step can always be read out from any bound δ-variable in its scope: If there are j γ-quantifiers between the quantifier for y inclusively and the quantifier for the δ-variable, the value for y is the j^{th} argument of the bound δ-variable, counting from the last argument backwards.

For instance, in the previous reduction step, the variable y in the third line was replaced with w^{δ} , the last argument of the bound δ-variable m^{δ}(v^{δ}, w^{δ}) , being first in the scope of y.

This property is obvious from Herbrand’s proof but hard to express as a property of proof normalization.

Moreover, this property is useful in Herbrand’s proof for showing that the side condition of the Rule of γ-Quantification \frac{B\{x↦t\}}{∃x. B} is always satisfied, even for a certain prenex form. Indeed, γ-variables never occur in the replacement t and the height of t is strictly smaller than the height of all bound δ-variables in the scope B, so that no free variable in t can be bound by quantifiers in B; cf. § 9.

100Roughly speaking, we may do a proof by hand, count the lemma applications and remember their instantiations, and then try to construct a formal normal form proof accordingly, just as we have done in Example 13.2. See [Wirth, 2004] for more on this.

101Roughly speaking, we may compute the connections and search for a reductive proof in the style of say [Wallen, 1990], which we then transform into a proof in the normal form of Statement 2 of Theorem 12.1.

102Even without the avoidance of the detour over prenex forms due to Heijenoort’s correction, this already

The normal form of proofs — as given by Lemma 13.1 — eliminates detours via modus ponens in a similar fashion as Gentzen’s Hauptsatz eliminates the Cut. It is remarkable not only because it establishes a connection between Skolem terms and free variables without using any semantics for Skolem functions (and thereby, without using the Axiom of Choice). It also seems to be the first time that a normal form of proofs is shown to exist in which different phases are considered. Even with Gentzen’s Verschärfter Hauptsatz following Herbrand in this aspect some years later, the concrete form of Herbrand’s normal form of proofs remains important to this day, especially in the form of Heijenoort’s correction, cf. § 11. The manner in which modern sequent, tableau, and matrix calculi organize proof search^{103} does not follow the Hilbert school and their ε-elimination theorems, but Gentzen’s and Herbrand’s calculi. Moreover, regarding their Skolemization, their deep inference,^{104} and their focus on γ-quantifiers and their multiplicity, these modern proof-search calculi are even more in Herbrand’s tradition than in Gentzen’s.

14 The Löwenheim–Skolem Theorem and Herbrand’s Finitistic Notion of Falsehood in an Infinite Domain

Let A be a first-order formula whose terms have a height not greater than m. Herbrand defines that A is false in an infinite domain if A does not have Property C of order p for any positive natural number p.

If, for a given positive natural number p, the formula A does not have Property C of order p, then we can construct a finite structure over the domain T_{p+m} which falsifies A^{T_{p}}; cf. § 7. Thus, instead of requiring a single infinite structure in which A^{T_{p}} is false for any positive natural number p, Herbrand’s notion of falsehood in an infinite domain only provides us, for each p, with a finite structure in which A^{T_{p}} is false. Herbrand explicitly points out that these structures do not have to be extensions of each other. From a given falsifying structure for some p one can, of course, generate falsifying structures for each p′ < p by restriction to T_{p′+m}. Herbrand thinks, however, that to require an infinite sequence of structures to be a sequence of extensions would necessarily include some form of the Axiom of Choice, which he rejects out of principle. Moreover, he writes that the basic prerequisites of the Löwenheim–Skolem Theorem are generally misunderstood, but does not make this point clear.

It seems that Herbrand reads [Löwenheim, 1915] as if it would be a paper on provability instead of validity, i.e. that Herbrand confuses Löwenheim’s ‘⊧’ with Herbrand’s ‘⊢’.

All in all, this is, on the one hand, so peculiar and, on the other hand, so relevant for Herbrand’s finitistic views of logic and proof theory that some quotations may illuminate the controversy.

holds for the normal form given by Statement 3 of Theorem 12.1, which is extensionally equal to Herbrand’s original Property A. The next further steps to improve this support for proof search would be sequents and free γ- and δ-variables; cf. e.g. [Wirth, 2004; 2008].

103Cf. e.g. [Wallen, 1990], [Wirth, 2004], [Autexier, 2005].

104Note that although the deep inference rules of Generalized Quantification are an extension of Herbrand’s calculi by Heijenoort, the deep inference rules of Passage and of Generalized Simplification are Herbrand’s original contributions.

“(On remarquera que cette définition diffère de la définition qu’on pourrait croire la plus naturelle seulement par le fait que, quand le nombre p augmente, le nouveau champ C′ et les nouvelles valeurs ne peuvent pas forcément être considérés comme un ‘prolongement’ des anciens; mais cependant, la connaissance de C′ et des valeurs pour un nombre p déterminé, entraîne celle d’un champ et de valeurs convenant pour tout nombre inférieur; seul donc un ‘principe de choix’ pourrait conduire à prendre un système de valeurs fixe dans un champ infini).”^{105}

After defining the dual notion for unsatisfiability instead of validity, Herbrand continues:

“Il est absolument nécessaire de prendre de telles définitions, pour donner un sens précis aux mots: ‘vrai dans un champ infini’, qui ont souvent été employés sans explication suffisante, et pour justifier une proposition à laquelle on fait souvent allusion, démontrée par Löwenheim,^{1} sans bien remarquer que cette proposition n’a aucun sens précis sans définition préalable, et que la démonstration de Löwenheim est au surplus totalement insuffisante pour notre but (voir 6.4).”^{106}

Herbrand’s Fundamental Theorem equates provability with Property C, whereas the Löwenheim–Skolem Theorem equates validity with Property C. Thus, it is not the case that Herbrand somehow corrected Löwenheim. Instead, the Löwenheim–Skolem Theorem and Herbrand’s Fundamental Theorem had better be looked upon as a bridge from validity to provability with two arcs and Property C as the eminent pillar in the middle of the river, offering a magnificent view from the bridge on properties of first-order logic; as depicted in § 12. And this was probably also Herbrand’s view when he correctly wrote:

“Nous pouvons dire que la démonstration de Löwenheim était suffisante en Mathématiques; mais il nous a fallu, dans ce travail, la rendre ‘métamathématique’ (voir l’introduction), pour qu’elle nous soit de quelque utilité.”^{107} Moreover, Herbrand criticizes Löwenheim for not showing the consistency of first-order logic, but this, of course, was never Löwenheim’s concern.

105Cf. [Herbrand, 1930, p.109]. Without the comma after “déterminé” also in: [Herbrand, 1968, p.135f.]

“We observe that this definition differs from the definition that would seem the most natural only in that, as the number p increases, the new domain C′ and the new values need not be regarded as forming an ‘extension’ of the previous ones. Clearly, if we know C′ and the values for a given number p, then for each smaller number we know a domain and values that answer to the number; but only a ‘principle of choice’ could lead us to take a fixed system of values in an infinite domain.” [Herbrand, 1971, p.165, translation by Dreben and Heijenoort] 106Cf. [Herbrand, 1930, p.110]. Without the signs after “définitions”, “mots”, and “préalable” and the emphasis on “Löwenheim ”, but with the correct “6.2” instead of the misprint “6.4” also in: [Herbrand, 1968, p.136f.]

“It is absolutely necessary to adopt such definitions if we want to give a precise sense to the words ‘true in an infinite domain’, words that have frequently been used without sufficient explanation, and also if we want to justify a proposition proved by Löwenheim, a proposition to which many refer without clearly seeing that Löwenheim’s proof is totally inadequate for our purposes (see 6.4) and that, indeed, the proposition has no precise sense until such a definition has been given.” [Herbrand, 1971, p.166, translated by Dreben and Heijenoort] 107Cf. [Herbrand, 1930, p.118]. Without the emphasis on “Löwenheim ” and with “mathématiques” instead of “Mathématiques” and “l’Introduction)” instead of “l’introduction),” also in: [Herbrand, 1968, p.144].

“We could say that Löwenheim’s proof was sufficient in mathematics; but, in the present work, we had to make it ‘metamathematical’ (see Introduction) so that it would be of some use to us.” [Herbrand, 1971, p.176, translated by Dreben and Heijenoort]

The mathematically substantial part of Herbrand’s critique of Löwenheim refers to the use of the Axiom of Choice in Löwenheim’s proof of the Löwenheim–Skolem Theorem.

The Löwenheim–Skolem Theorem as found in many textbooks, such as [Enderton, 1972, p.141], says that any satisfiable set of first-order formulas is satisfiable in a countable structure. In [Löwenheim, 1915], however, we only find a dual statement, namely that any invalid first-order formula has a denumerable counter-model. Moreover, what is actually proved, read charitably,^{108} is the following stronger theorem:

Theorem 14.1 (Löwenheim–Skolem Theorem à la Löwenheim [1915]) Let us assume the Axiom of Choice. Let A be a first-order formula.

1. If A has Property C of order p for some positive natural number p, then ⊧ A.

2. If A does not have Property C of order p for any positive natural number p, then we can construct a sequence of partial structures S_{i} that converges to a structure S′ with a denumerable universe such that |̸=_{S′} A. □

As Property C of order p can be effectively tested for p = 1, 2, 3, …, Löwenheim’s proof provides us with a complete proof procedure which went unnoticed by Skolem as well as the Hilbert school. Indeed, there is no mention in the discussion of the completeness problem for first-order logic in [Hilbert & Ackermann, 1928, p. 68], where it is considered as an open problem.^{109}

Thus, for validity instead of provability, Gödel’s Completeness Theorem^{110} is contained already in [Löwenheim, 1915]. Gödel has actually acknowledged this for the version of the proof of the Löwenheim–Skolem Theorem in [Skolem, 1923b].^{111}

Note that the convergence of the structures S_{i} against S′ in Theorem 14.1 is hypothetical in two aspects: First, as validity is not co-semi-decidable, in general we can never positively know that we are actually in Case 2 of Theorem 14.1, i.e. that a convergence toward S′ exists. Second, even if we knew about the convergence toward S′, we would have no general procedure to find out which parts of S_{i} will be actually found in S′ and which will be removed by backtracking. This makes it hard to get an intuition for S′ and may be the philosophical reason for Herbrand’s rejection of “falsehood in S′ ” as a meaningful notion. Mathematically, however, we see no justification in Herbrand’s rejection of this notion and will explain this in the following.

108As Löwenheim’s paper lacks some minor details, there is an ongoing discussion whether its proof of the Löwenheim–Skolem Theorem is complete and what is actually shown. Our reading of the proof of the Löwenheim–Skolem Theorem in [Löwenheim, 1915] is a standard one. Only in [Skolem, 1941, p. 26ff.] and [Badesa, 2004, § 6.3.4] we found an incompatible reading, namely that — to construct S′ of Item 2 of Theorem 14.1 — Löwenheim’s proof requires an additional falsifying structure of arbitrary cardinality to be given in advance. The similarity of our presentation with Herbrand’s Fundamental Theorem, however, is in accordance with [Skolem, 1941, p. 30], but not with [Badesa, 2004, p.145]. The relation of Herbrand’s Fundamental Theorem to the Löwenheim–Skolem Theorem is further discussed in [Anellis, 1991]. Cf. also our Note 113.

109Actually, the completeness problem is slightly ill defined in [Hilbert & Ackermann, 1928]. Cf. e.g.

[Gödel, 1986ff., Vol. I, pp. 44–48].

110Cf. [Gödel, 1930].

111Letter of Gödel to Heijenoort, dated Aug. 14, 1964. Cf. [Heijenoort, 1971a, p. 510, Note i], [Gödel, 1986ff., Vol. I, p. 51; Vol. V, pp. 315–317].

Herbrand’s critical remark concerning the Löwenheim–Skolem Theorem is justified, however, insofar as Löwenheim needs the Axiom of Choice at two steps in his proof without mentioning this.

1^{st} Step: To show the equivalence of a formula to its outer Skolemized form, Löwenheim’s proof requires the full Axiom of Choice.

2^{nd} Step: For constructing the structure S′, Löwenheim would need König’s Lemma, which is a weak form of the Axiom of Choice.^{112}

Contrary to the general perception,^{113} there are no essential gaps in Löwenheim’s proof, with the exception of the implicit application of the Axiom of Choice, which was no exception at his time. Indeed, fifteen years later, Gödel still applies the Axiom of Choice tacitly in the proof of his Completeness Theorem.^{114} Moreover, as none of these theorems state any consistency properties, from the point of view of Hilbert’s finitism there was no reason to avoid the application of the Axiom of Choice. Indeed, in the proof of his Completeness

112König’s Lemma is Form 10 in [Howard & Rubin, 1998]. This form is even weaker than the well-known Principle of Dependent Choice, namely Form 43 in [Howard & Rubin, 1998]; cf. also [Rubin & Rubin, 1985]. 113This perception is partly based on the unjustified criticism of Skolem, Herbrand, and Heijenoort. We are not aware of any negative critique against [Löwenheim, 1915] at the time of publication. [Wang,

1970, p. 27ff.], proof-read by Bernays and Gödel, after being most critical with the proof in [Skolem, 1923b], sees no gaps in Löwenheim’s proof, besides the applications of the Axiom of Choice. The same holds for [Brady, 2000, § 8], sharing expertise in the Peirce–Schröder tradition^{57} with Löwenheim.

Let us have a look at the criticism of Skolem, Herbrand, and Heijenoort in detail:

The following statement of Skolem on [Löwenheim, 1915] is confirmed in [Heijenoort, 1971a, p. 230]:

“Er muss also sozusagen einen Umweg über das Nichtabzählbare machen.”

[Skolem, 1923b, p. 220]

“Thus he must make a detour, so to speak, through the non-denumerable.”

[Heijenoort, 1971a, p. 293, translation by by Stefan Bauer-Mengelberg]

That detour, however, is not an essential part of the proof, but serves for the purpose of illustration only. This is clear from the original paper and also the conclusion in [Badesa, 2004, §§ 3.2 and 3.3].

When Herbrand criticizes Löwenheim’s proof, he actually does not criticize the proof as such, but only Löwenheim’s semantical notions; even though Herbrand’s verbalization suggests the opposite, especially in [Herbrand, 1931, Chapter 2], where Herbrand repeats Löwenheim’s reducibility results in finitistic style:

“Löwenheim [1915] a publié du résultat énoncé dans ce paragraphe une démonstration dont nous avons montré les graves lacunes dans notre travail déjà cité (Chapter 5, § 6.2).”

[Herbrand, 1968, p. 187, Note 29]

“Löwenheim [1915] published a proof of the result stated in this section. In [Herbrand, 1930, Chapter 5, § 6.2], we pointed out that there are serious gaps in his proof.”

[Herbrand, 1971, p. 237, Note 33, translation by Dreben and Heijenoort]

Heijenoort realized that there is a missing step in Löwenheim’s proof:

“What has to be proved is that, from the assignments thus obtained for all i, there can be formed one assignment such that ΠF is true, that is, ΠF = 0 is false. This Löwenheim does not do.” [Heijenoort, 1971a, p. 231]

Except for the principle of choice, however, the missing step is trivial because in Löwenheim’s presentation the already fixed part of the assignment is irrelevant for the extension. Indeed, in the “Note to the Second Printing”, in the preface of the 2^{nd} printing, Heijenoort partially corrected himself:

“I am now inclined to think that Löwenheim came closer to König’s Lemma than his paper, on the surface, suggests. But a rewriting of my introductory note on that point (p. 231) will have to wait for another occasion.” [Heijenoort, 1971a, p. ix]

This correction is easily overlooked because no note was inserted into the actual text.

114Cf. [Gödel, 1930].

Theorem, Gödel “is not interested in avoiding an appeal to the Axiom of Choice.”^{115} Thus, again, as we already noted in Item 2 of § 3, regarding finitism, Herbrand is more royalist than King Hilbert.

The proof of the Löwenheim–Skolem Theorem in [Skolem, 1920] already avoids the Axiom of Choice in the 1^{st} Step by using Skolem normal form instead of Skolemized form.^{116}

Moreover, in [Skolem, 1923b], the choices in the 2^{nd} Step of the proof become deterministic, so that no form of the Axiom of Choice (such as König’s Lemma) is needed anymore. This is achieved by taking the universe of the structure S′ to be the natural numbers and by using the well-ordering of the natural numbers.

Theorem 14.2 (Löwenheim–Skolem Theorem à la [Skolem, 1923b]) Let Γ be a (finite of infinite) denumerable set of first-order formulas. Assume |̸= Γ. Without assuming any form of the Axiom of Choice we can construct a sequence of partial structures S_{i} that converges to a structure S′ with a universe which is a subset of the natural numbers such that |̸=_{S′} Γ. □

Note that Herbrand does not need any form of the Axiom of Choice for the following reasons: In the 1^{st} Step, Herbrand does not use the semantics of Skolemized forms at all, because Herbrand’s Skolem terms are just names for free variables, cf. § 12. In the 2^{nd} Step, Herbrand’s peculiar notion of “falsehood in an infinite domain” makes any choice superfluous. This is a device which — contrary to what Herbrand wrote — is not really necessary to avoid the Axiom of Choice, as the above Theorem 14.2 shows.

In this way, Herbrand came close to proving the completeness of Russell’s and Hilbert’s calculi for first-order logic, but he did not trust the left arc of the bridge depicted in § 12. And thus Gödel proved it first when he submitted his thesis in 1929, in the same year as Herbrand, and the theorem is now called Gödel’s Completeness Theorem in all textbooks on logic.^{117}

It is also interesting to note that Herbrand does not know how to construct a countermodel without using the Axiom of Choice, as explicitly described in [Skolem, 1923b]. This is — on the one hand — a strong indication that Herbrand was not aware of [Skolem, 1923b].^{118} On the other hand, Herbrand names Skolem’s Paradox several times and [Skolem, 1923b; 1929] seem to be the only written sources of this at Herbrand’s time.^{119}

As Herbrand’s Property C and its use of the outer Skolemized form are most similar to the treatment in [Skolem, 1928], it seems likely that Herbrand had read [Skolem, 1928].^{120}

115Cf. [Wang, 1970, p. 24].

116To achieve Skolem normal form, Skolem defines predicates for the subformulas starting with a γ-quantifier, and then rewrites the formula into a prenex form with a first-order γ^{∗}δ^{∗}-prefix. Indeed, for the proofs of the versions of the Löwenheim–Skolem Theorem, the Skolemized form (which is used in [Löwenheim, 1915], [Skolem, 1928], and [Herbrand, 1930]) is used neither in [Skolem, 1920] nor in [Skolem, 1923b], which use Skolem normal form instead.

By definition, Skolemized forms have a δ^{∗}γ^{∗}-prefix with an implicit higher-order δ^{∗}, and raising is the dual of Skolemization which produces a γ^{∗}δ^{∗}-prefix with a higher-order γ^{∗}, cf. [Miller, 1992]. The Skolem normal form, however, has a γ^{∗}δ^{∗}-prefix with first-order γ^{∗}.

117Cf. [Gödel, 1930].

118Cf. p.12 of Goldfarb’s introduction in [Herbrand, 1971].

119Skolem’s Paradox is also briefly mentioned in [Neumann, 1925], not as a paradox, however, but as unfavorable conclusions on set theory drawn by Skolem, who wrote about a “peculiar and apparently paradoxical state of affairs”, cf. [Heijenoort, 1971a, p. 295].

120Without giving any justification, Heijenoort assumes, however, that

“He was not acquainted either, certainly, with [Skolem, 1928].” [Heijenoort, 1986c, p.112]

15 Herbrand’s First Proof of the Consistency of Arithmetic

Consider a signature of arithmetic that consists only of zero ‘0’, the successor function ‘s’, and the equality predicate ‘=’. Besides the axioms of equality (equivalence and substitutability), Herbrand considers several subsets of the following axioms:^{121}

(S)  P (0) ∧ ∀y. ( P (y) ⇒ P (s(y)) ) ⇒ ∀x. P (x)
(nat_{1})  x = 0 ∨ ∃y. x = s(y)
(nat_{2})  s(x) ≠ 0
(nat_{3})  s(x) = s(y) ⇒ x = y
(nat_{4+i}) s^{i+1}(x) ≠ x

Axiom (nat_{1}) together with the well-foundedness of the successor relation ‘s’ specifies the natural numbers up to isomorphism.^{122} So do the Dedekind–Peano axioms (nat_{2}) and (nat_{3}) together with the Dedekind–Peano axiom of Structural Induction (S), provided that the meta variable P is seen as a universally quantified second-order variable with the standard interpretation.^{123}

Of course, Herbrand, the finitist, does not even mention these second-order properties. His discussion is restricted to decidable first-order axiom sets, some of which are infinite due to the inclusion of the infinite sequence (nat_{4}), (nat_{5}), (nat_{6}), …

As Herbrand’s axiom sets are first order, they cannot specify the natural numbers up to isomorphism.^{124} But as the model of arithmetic is infinite, Herbrand, the finitist, cannot accept it as part of his proof theory. Actually, he never even mentions the model of arithmetic.

Herbrand shows that (for the poor signature of 0, s, and =) the first-order theory of the axioms (nat_{i})_{i≥1} (i.e. (nat_{i}) for any positive natural number i) is consistent, complete, and decidable. His constructive proof is elegant, provides a lucid operative understanding of basic arithmetic, and has been included inter alia into § 3.1 of [Enderton, 1972], one of the most widely used textbooks on logic. Herbrand’s proof has two constructive steps:

1^{st} Step: He shows how to rewrite any formula into an equivalent quantifier-free formula without additional free variables. He proceeds by a special form of quantifier elimination, a technique in the Peirce–Schröder tradition^{57} with its first explicit occurrence in [Skolem, 1919].^{125}

2^{nd} Step: He shows that the quantifier-free fragment is consistent and decidable and does not depend on the axiom (nat_{1}). This is achieved with a procedure which rewrites a quantifier-free formula into an equivalent disjunctive normal form without additional free variables. For any quantifier-free formula B, this normal-form procedure satisfies: (nat_{i})_{i≥2} ⊢ B iff the normal form of ¬B is 0 ≠ 0.

121The labels are ours, not Herbrand’s. Herbrand writes ‘x+1’ instead of ‘s(x)’. To save the axiom of substitutability, Herbrand actually uses the biconditional in (nat_{3}).

122Cf. [Wirth, 2004, § 1.1.3]. This idea goes back to [Pieri, 1907/8].

123Cf. e.g. [Andrews, 2002].

124For instance, due to the Upward Löwenheim–Skolem–Tarski Theorem. Cf. e.g. [Enderton, 1972].

125More precisely, cf. [Skolem, 1919, § 4]. For more information on the subject of quantifier elimination in this context, cf. [Anellis, 1992, p.120f., Note 33], [Wang, 1970, p. 33].

This elegant work of Herbrand is hardly discussed in the secondary literature, probably because — as a decidability result — it became obsolete before it was published, due to the analogous result for this theory extended with addition, the so-called Presburger Arithmetic, as it is known today. Mojżesz Presburger (1904–1943?)^{126} gave his talk on the decidability of his theory with similar techniques on Sept. 24, 1929,^{127} five months after Herbrand finished his PhD thesis. As Tarski’s work on decision methods developed in his 1927/8 lectures in Warszawa also did not appear in print until after World War II,^{128} we have to consider this contribution of Herbrand as completely original. Indeed:

“Dieses gelingt nach einer Methode, welche unabhängig voneinander J. Herbrand und M. Presburger ausgebildet haben. Diese Methode besteht darin, dass man Formeln, welche gebundene Variablen enthalten, ’Reduzierte‘ zuordnet, in denen keine gebundenen Variablen mehr auftreten und welche im Sinne der inhaltlichen Deutung jenen Formeln gleichwertig sind.”^{129}

In addition, Herbrand gives a constructive proof that the first-order theories given by the following two axiom sets are identical:

• (nat_{i})_{i≥1}

• (nat_{2}), (nat_{3}), and the first-order instances of (S), provided that (S) is taken as a first-order axiom scheme instead of a second-order axiom.

16 Herbrand’s Second Proof of the Consistency of Arithmetic

Herbrand’s contributions to logic discussed so far are all published in Herbrand’s thesis. In this section, we consider his journal publication [Herbrand, 1932a] as well as some material from Chapter 4 of his thesis.

First, the signature is now enriched to include the recursive functions, cf. § 17. Second, the axiom scheme (S) is restricted to just those instances which result from replacing the meta variable P with quantifier-free first-order formulas. For this setting, Herbrand again gives a constructive proof of consistency. This proof consists of the following two steps:

126Presburger’s true name is Prezburger. He was a student of Alfred Tarski, Jan Łukasiewicz (1878– 1956), Kazimierz Ajdukiewicz (1890–1963), and Kazimierz Kuratowski (1896–1980) in Warszawa. He was awarded a master (not a PhD) in mathematics on Oct. 7, 1930. As he was of Jewish origin, it is likely that he died in the Holocaust (Shoah), maybe in 1943. Cf. [Zygmunt, 1991].

127Moreover, note that [Presburger, 1930] did not appear in print before 1930. Some citations date [Presburger, 1930] at 1927, 1928, and 1929. There is evidence, however, that these earlier datings are wrong, cf. [Stanisfer, 1984], [Zygmunt, 1991].

128Cf. [Stanisfer, 1984], [Tarski, 1951].

129Cf. [Hilbert & Bernays, 1968/70, Vol. I, p. 233, note-mark omitted, orthography modernized].

“This is achieved by a method developed independently by J. Herbrand and M. Presburger. The

method consists in associating ‘reduced forms’ to formulas with bound variables, in which no

bound variables occur anymore and which are semantically equivalent to the original formulas.”

1^{st} Step: Herbrand defines recursive functions f_{P} such that f_{P} (x) is the least natural number y ≤ x such that ¬P (y) holds, provided that such a y exists, and 0 otherwise. The functions f_{P} are primitive recursive unless the terms substituted for P contain a non-primitive recursive function. These functions imply the instances of (S), rendering them redundant. This is similar to the effect of Hilbert’s 2^{nd} ε-formula:^{130}

εx.¬P (x) = s(y) ⇒ P (y), Herbrand’s procedure, however, is much simpler but only applicable to quantifierfree P.

2^{nd} Step: Consider the universal closures of the axioms of equality, the axioms (nat_{2}) and (nat_{3}), and an arbitrary finite subset of the axioms for recursive functions. Take the negation of the conjunction of all these formulas. As all quantified variables of the resulting formula are γ-variables, this is already in Skolemized form. Moreover, for any positive natural number n, it is easy to show that this formula does not have Property C of order n: Indeed, we just have to construct a proper finite substructure of arithmetic which satisfies all the considered axioms for the elements of T_{n}. Thus, by Herbrand’s Fundamental Theorem, consistency is immediate.

The 2^{nd} step is a prototypical example to demonstrate how Herbrand’s Fundamental Theorem helps to answer seemingly non-finitistic semantical questions on infinite structures with the help of infinitely many finite sub-structures. Notice that such a semantical argumentation is finitistically acceptable if and only if the structures are all finite and effectively constructible. And the latter is always the case for Herbrand’s work on logic.

As the theory of all recursive functions is sufficiently expressive, there is the question why Herbrand’s second consistency proof does not imply the inconsistency of arithmetic by Gödel’s 2^{nd} incompleteness theorem? Herbrand explains that we cannot have the theory of all total recursive functions because they are not recursively enumerable. More precisely, an evaluation function for an enumerable set of recursive functions cannot be contained in this set by the standard diagonalization argument.

Hilbert’s school had failed to prove the consistency of arithmetic, except for the special case that for the axiom (S), the variable x does not occur within the scope of any binder in P (x).^{131} But this fragment of arithmetic is actually equivalent to the one considered by Herbrand here.^{132} In this sense, Herbrand’s result on the consistency of arithmetic was just as strong as the one of the Hilbert school by ε-substitution. Herbrand’s means, however, are much simpler.^{133}

130Cf. [Hilbert & Bernays, 1968/70, Vol. II, § 2.3, p. 82ff.; Vol. II, Supplement V B, p. 535ff.].

131Cf. [Hilbert & Bernays, 1968/70, Vol. II, § 2.4].

More precisely, Hilbert’s school had failed to prove the termination of their first algorithm for computing a valuation of the ε-terms in the 1^{st} and 2^{nd} ε-formulas. This de facto failure was less spectacular but internally more discouraging for Hilbert’s programme than Gödel’s 2^{nd} incompleteness theorem with its restricted area of application, cf. [Gödel, 1931].

Only after developing a deeper understanding of the notion of a basic typus of an ε-term (Grundtypus; introduced in [Neumann, 1927]; called ε-matrix in [Scanlon Jr., 1973]) and especially of the independence of its valuation of the valuations of its sub-ordinate ε-expressions, has the problem been resolved: The termination problem was cured in [Ackermann, 1940] with the help of a second algorithm of ε-valuation, terminating within the ordinal number ϵ_{0}, just as Gentzen’s consistency proof for full arithmetic in [Gentzen, 1936; 1938; 1943].

132Cf. [Kleene, 1952, p. 474].

17 Foreshadowing Recursive Functions

Herbrand’s notion of a recursive function is quite abstract: A recursive function is given by any new n_{i}-ary function symbol f_{i} plus a set of quantifier-free formulas for its specification (which Herbrand calls the hypotheses), such that, for any natural numbers k_{1}, …, k_{n_{i}}, there is a constructive proof of the unique existence of a natural number l such that

⊢ f_{i}(s^{k_{1}}(0), …, s^{k_{n_{i}}}(0)) = s^{l}(0).

“On pourra aussi introduire un nombre quelconque de fonctions f_{i}x_{1}x_{2} ⋯ x_{n_{i}} avec des hypothèses telles que:

a) Elles ne contiennent pas de variables apparentes.

b) Considérées intuitionnistiquement,^{5} elles permettent de faire effectivement le calcul de f_{i}x_{1}x_{2} ⋯ x_{n_{i}}, pour tout système particulier de nombres; et l’on puisse démontrer intuitionnistiquement que l’on obtient un résultat bien déterminé. (Groupe C.)

5Cette expression signifie: traduites en language ordinaire, considérées comme une propriété des entiers, et non comme un pur symbole.”

[Herbrand, 1932a, p. 5]^{134}

In the letter to Gödel dated April 7, 1931, mentioned already in § 2, Herbrand added the requirement that the hypotheses defining f_{i} contain only function symbols f_{j} with j≤i, for natural numbers i and j.^{135}

Gödel’s version of Herbrand’s notion of a recursive function is a little different: He speaks of quantifier-free equations instead of quantifier-free formulas and explicitly lists the already known functions, but omits the computability of the functions:

133Herbrand’s results on the consistency of arithmetic have little importance, however, for today’s inductive theorem proving because the restrictions on (S) can usually not be met in practice. Herbrand’s restrictions on (S) require us to avoid the occurrence of x in the scope of quantifiers in P (x). In practice of inductive theorem proving, this is hardly a problem for the γ-quantifiers, whose bound variables tend to be easily replaceable with witnessing terms. There is a problem, however, with the δ-quantifiers. If we remove the δ-quantifiers, letting their bound δ-variables become free δ-variables, the induction hypothesis typically becomes too weak for proving the induction step. This is because the now free δ-variables do not admit different instantiation in the induction hypotheses and the induction conclusion. 134Without the colon after “que” and the comma after “f_{i}x_{1}x_{2} ⋯ x_{n_{i}}”, with a semi-colon instead of a full-stop after “apparentes”, and with “langage” instead of “language” also in: [Herbrand, 1968, p. 226f.]

“We can also introduce any number of functions f_{i}(x_{1}, x_{2}, …, x_{n_{i}}) together with some hypotheses such that

(a) The hypotheses contain no bound variables.

(b) Considered intuitionistically,^{5} they make the effective computation of the f_{i}(x_{1}, x_{2}, …, x_{n_{i}}) possible for every given set of numbers, and it is possible to prove intuitionistically that we obtain a well-defined result. (Group C.)

5This expression means: translated into ordinary language, considered as a property of integers and not as a mere symbol.”

135Cf. [Gödel, 1986ff., Vol. V, pp. 14–21], [Sieg, 2005].

“If ϕ denotes an unknown function and ψ_{1}, …, ψ_{k} are known functions, and if the ψ’s and the ϕ are substituted in one another in the most general fashions and certain pairs of the resulting expressions are equated, then, if the resulting set of functional equations has one and only one solution for ϕ, ϕ is a recursive function.”^{136}

Gödel took this paragraph on page 26 of his 1934 Princeton lectures from the abovementioned letter from Herbrand to Gödel, which Gödel considered to be lost, but which was rediscovered in February 1986.^{137} In 1963, Gödel wrote to Heijenoort:

“I have never met Herbrand. His suggestion was made in a letter in 1931, and it was formulated exactly as on p. 26 of my lecture notes, that is, without any reference to computability. However, since Herbrand was an intuitionist, this definition for him evidently meant that there is a constructive proof for the existence and uniqueness of ϕ.”^{138}

As we have seen, however, Gödel’s memory was wrong insofar as he had added the restriction to equations and omitted the computability requirement.

Obviously, Herbrand had a clear idea of our current notion of a total recursive function. Herbrand’s characterization, however, just transfers the recursiveness of the meta level to the object level. Such a transfer is of little epistemological value. While there seems to be no way to do much more than such a transfer for consistency of arithmetic in Gödelizable systems (due to Gödel’s 2^{nd} incompleteness theorem), it is well possible to do more than that for the notion of recursive functions. Indeed, in the later developments of the theory of term rewriting systems and the today standard recursion theory for total and partial recursive functions, we find constructive definitions and consistency proofs practically useful in programming and inductive theorem proving.^{139} Thus, as suggested by Gödel,^{140} we may say that Herbrand foreshadowed the notion of a recursive function, although he did not introduce it.^{141}

136Cf. [Gödel, 1934, p. 26], also in: [Gödel, 1986ff., Vol. I, p. 368].

137Cf. [Dawson Jr., 1993].

138Letter of Gödel dated April 23, 1963. Cf. [Herbrand, 1971, p. 283], also in: [Heijenoort, 1986c, p.115f.], also in: [Gödel, 1986ff., Vol. V, p. 308].

It is not clear whether Gödel refers to Brouwer’s intuitionism or Hilbert’s finitism when he calls Herbrand an “intuitionist” here; cf. § 3.

And there is more confusion regarding the meaning of two occurrences of the word “intuitionistically” on the page of the above quotation from [Herbrand, 1932a]. Both occurrences carry the same note-mark, probably because Herbrand realized that this time he uses the word with even a another meaning, different from his own standard and different from its meaning for the other occurrence in the same quotation: It neither refers to Brouwer’s intuitionism nor to Hilbert’s finitism, but actually to the working mathematician’s meta level as opposed to the object level of his studies; cf. e.g. [Neumann, 1927, p. 2f.].

139Partial recursive functions were introduced in [Kleene, 1938]. For consistency proofs and admissibility conditions for the practical specification of partial recursive functions with positive/negative-conditional term rewriting systems cf. [Wirth, 2009].

140Letter of Gödel to Heijenoort, dated Aug. 14, 1964. Cf. [Heijenoort, 1986c, p.115f.].

141Cf. [Heijenoort, 1986c, p.115ff.] for more on this. Moreover, note that a general definition of (total)

recursive functions was not required for Herbrand’s second consistency proof because Herbrand’s function f_{P} of § 16 is actually a primitive recursive one, unless P contains a non-primitive recursive function.

18 Herbrand’s Influence on Automated Deduction and Herbrand’s Unification Algorithm

In the last fifty years the field of automated deduction, or automated reasoning as it is more generally called today, has come a long way: modern deduction systems are among the most sophisticated and complex human artefacts we have, they can routinely search spaces of several million formulas to find a proof. Automated theorem proving systems have solved open mathematical problems and these deduction engines are used nowadays in many subareas of computer science and artificial intelligence, including software development and verification as well as security analysis. The application in industrial software and hardware development is now standard practice in most high quality products. The handbook [Robinson & Voronkow, 2001] gives a good impression of the state of the art today.

Herbrand’s work inspired the development of the first computer programs for automated deduction and mechanical theorem proving, for the following reason: The actual test for Herbrand’s Property C is very mechanical in nature and thus can be carried out on a computer, resulting in a mechanical semi-decision procedure for any mathematical theorem! This insight, first articulated in the 1950s, turned out to be most influential in automated reasoning, artificial intelligence, and computer science.

Let us recapitulate the general idea as it is common now in most monographs and introductory textbooks on automated theorem proving.

Suppose we are given a conjecture A. Let F be its (validity) Skolemized form; cf. § 8. We then eliminate all quantifiers in F, and the result is a quantifier-free formula E. We now have to show that the Herbrand disjunction over some possible values of the free variables of E is valid. See also Example 10.2 in § 10.

How do we find these values? Well, we do not actually have these “objects in the domain”, but we can use their names, i.e. we take all terms from the Herbrand universe and substitute them in a systematic way into the variables and wait what happens: every substituted formula obtained that way is sentential, so we can just check whether their disjunction is valid or not with one of the many available decision procedures for sentential logic. If it is valid, we are done: the original formula A must be valid by Herbrand’s Fundamental Theorem. If the disjunction of instantiated sentential formulas turns out to be invalid, well, then bad luck and we continue the process of substituting terms from the Herbrand universe.

This process must terminate, if indeed the original theorem is valid. But what happens if the given conjecture is in fact not a theorem? Well, in that case the process will either run forever or sometimes, if we are lucky, we can nevertheless show this to be the case.

In the following we will present these general ideas a little more technically.^{142} Arithmetic provided a testbed for the first automated theorem proving program: In 1954 the program of Martin Davis (born 1928) proved the exciting theorem that the sum of two even numbers is again even. This date is still considered a hallmark and was used as the date for the 50^{th} anniversary of automated reasoning in 2004. The system that proved this and other theorems was based on Presburger Arithmetic, a decidable fragment of first-order logic, mentioned already in § 15.

142Standard textbooks covering the early period of automated deduction are [Chang & Lee, 1973] and [Loveland, 1978]. Chang & Lee [1973] present this and other algorithms in more detail and rigor.

Another approach, based directly on Herbrand’s ideas, was tried by Paul C. Gilmore (born 1925).^{143} His program worked as follows: A preprocessor generated the Herbrand disjunction in the following sense. The formula E contains finitely many constant and function symbols, which are used to systematically generate the Herbrand universe for this set; say

a, b, f(a, a), f(a, b), f(b, a), f(b, b), g(a, a), g(a, b), g(b, a), g(b, b), f(a, f(a, a)), …

for the constants a, b and the binary function symbols f, g. The terms of this universe were enumerated and systematically substituted for the variables in E such that the program generates a sequence of propositional formulas Eσ_{1}, Eσ_{2}, … where σ_{1}, σ_{2}, … are the substitutions. Now each of these sets can be checked for truth-functional validity, for which Gilmore used the “multiplication method”. This method computes the conjunctive normal form^{144} and checks the individual elements of this conjunction in turn: If any element contains the disjunction of an atom and its negation, it must be true and hence can be removed from the overall conjunction. As soon as all disjunctions have been removed, the theorem is proved — else it goes on forever.

This method is not particularly efficient and served to prove a few very simple theorems only. Such algorithms became known as British Museum Algorithms. That name was originally justified as follows:

“Thus we reflect the basic nature of theorem proving; that is, its nature prior to building up sophisticated proof techniques. We will call this algorithm the British Museum Algorithm, in recognition of the supposed originators of this type.” [Newell &al., 1957]

The name has found several more popular explanations since. The nicest is the following: If monkeys are placed in front of typewriters and they type in a guaranteed random fashion, they will reproduce all the books of the library of the British Museum, provided they could type long enough.

143Cf. [Gilmore, 1960]. The idea is actually due to Löwenheim and Skolem besides Herbrand, as discussed in detail in § 14 .

144Actually, the historic development of automated theorem proving did not follow Herbrand but Skolem in choosing the duality validity–unsatisfiablity. Thus, instead of proving validity of a conjecture, the task was to show unsatisfiablity of the negated conjecture. For this reason, Gilmore actually used the disjunctive normal form here.

A few months later Martin Davis and Hilary Putnam (born 1926) experimented with a better idea, where the multiplication method is replaced by what is now known as the Davis–Putnam procedure.^{145} It works as follows: the initial formula E is transformed (once and for all) into disjunctive normal form and then the variables are systematically replaced by terms from the Herbrand universe as before. But now the truth-functional check is replaced with a very effective procedure, which constituted a huge improvement and is still used today in many applications involving propositional logic.^{146} However, the most cumbersome aspect remained: the systematic but blind replacement of variables by terms from the Herbrand universe. Could we not find these replacements in a more goal-directed and intelligent way?

The first step in that direction was done by Davis [1963] in a method called linked conjuncts, where the substitution was cleverly chosen, so that it generated the desired tautologies more directly. And this idea finally led to the seminal resolution principle discovered by J. Alan Robinson (born 1930), which dominated the field ever since.^{147}

This technique — called a machine-oriented logic by Robinson — dispenses with the systematic replacement from the Herbrand universe altogether and finds the proper substitutions more directly by an ingenious combination of Cut and a unification algorithm. It works as follows: first transform the formula E into disjunctive normal form, i.e. into a disjunctive set of conjunctions. Now suppose that the following elements are in this disjunctive set:

K_{1} ∧ … ∧ K_{m} ∧ L and ¬L ∧ M_{1} ∧ … ∧ M_{n}.

Then we can add their resolvent

K_{1} ∧ … ∧ K_{m} ∧ M_{1} ∧ … ∧ M_{n}

to this disjunction, simply because one of the previous two must be true if the resolvent is true.

Now suppose that the literals L and ¬L are not already complementary because they still contain variables, for example such as P (x, f(a, y)) and ¬P (a, f(z, b)). It is easy to see, that these two atoms can be made equal, if we substitute a for the variables x and z and the constant b for the variable y. The most important aspect of the resolution principle is that this substitution can be computed by an algorithm, which is called unification. Moreover, there is always at most one (up to renaming) most general substitution which unifies two atoms, and this single unifier stands for the potentially infinitely many instances from the Herbrand universe that would be generated otherwise.

Robinson’s original unification algorithm is exponential in time and space. The race for the fastest unification algorithm lasted more than a quarter of a century and resulted in a linear algorithm and unification theory became a (small) subfield of computer science, artificial intelligence, logic, and universal algebra.^{148}

145Cf. [Davis & Putnam, 1960].

146Cf. The international SAT Competitions web page http://www.satcompetition.org/.

147Cf. [Robinson, 1965].

148Cf. [Siekmann, 1989] for a survey.

Unification theory had its heyday in the late 1980s, when the Japanese challenged the Western economies with the “Fifth Generation Computer Programme” which was based among others on logical programming languages. The processors of these machines realized an ultrafast unification algorithm cast in silicon, whose performance was measured not in MIPS (machine instructions per second), as with standard computers, but in LIPS (logical inferences per second, which amounts to the number of unifications per second). A myriad of computing machinery was built in special hardware or software on these new concepts and most industrial countries even founded their own research laboratories to counteract the Japanese challenge.^{149}

Interestingly, Jacques Herbrand had seen the concept of a unifying substitution and an algorithm already in his thesis in 1929. Here is his account in the original French idiom:

“1^{0}. Si une des égalités à satisfaire égale une variable restreinte x à un autre individu; ou bien cet individu contient x, et on ne peut y satisfaire; ou bien il ne contient pas x; cette égalité sera alors une des égalités normales cherchées; et on remplacera x par cette fonction dans les autres égalités à satisfaire.

2^{0}. Si une des égalités à satisfaire égale une variable générale à un autre individu, qui ne soit pas une variable restreinte, il est impossible d’y satisfaire.

3^{0}. Si une des égalités à satisfaire égale

f_{1}(φ_{1}, φ_{2}, …, φ_{n}) à f_{2}(ψ_{1}, ψ_{2}, …, ψ_{m}), ou bien les fonctions élémentaires f_{1} et f_{2} sont différentes, auquel cas il es impossible d’y satisfaire; ou bien les fonctions f_{1} et f_{2} sont les mêmes; auquel cas on remplace l’égalité par celles obtenues en égalant φ_{i} à ψ_{i}.”^{150}

149Such as the European Computer-Industry Research Center (ECRC), which was supported by the French company Bull, the German Siemens company, and the British company ICL.

150Cf. [Herbrand, 1930, p. 96f.]. Note that the reprint in [Herbrand, 1968, p.124] has “associées” instead of “normales”, which is not an improvement, and the English translation of [Herbrand, 1971, p.148] is based on this contorted version.

“1. If one of the equations to be satisfied equates a γ-variable x^{γ} to another term; either this term

contains x^{γ}, and then the equation cannot be satisfied; or else the term does not contain x^{γ}, and then the equation will be one of the normal-form equations we are looking for, and we replace x^{γ} by the term in the other equations to be satisfied.

2. If one of the equations to be satisfied equates a δ-variable to another term that is not a

γ-variable, the equation cannot be satisfied.

3. If one of the equations to be satisfied equates f_{1}(φ_{1}, φ_{2}, …, φ_{n}) to f_{2}(ψ_{1}, ψ_{2}, …, ψ_{m}); either

the function symbols f_{1} and f_{2} are different, and then the equation cannot be satisfied; or they are the same, and then we replace this equation with those that equate φ_{i} to ψ_{i}.”

19 Conclusion

With regard to students interested in logic, in the previous lectures we have presented all major contributions of Jacques Herbrand to logic, and our 150 notes give hints on where to continue studying.

With regard to historians, we uncovered some parts of the historical truth on Herbrand which was varnished by contemporaries such as Gödel and Heijenoort. It was already wellknown that Gödel’s memories on Herbrand’s recursive functions were incorrect, but to the best of our knowledge the errors of the reprint of Herbrand’s PhD thesis [Herbrand, 1930] in [Herbrand, 1968] have not been noted before. The English translation in [Herbrand, 1971] is based on this contorted reprint: The advantage of working with the original prints should become obvious from a comparison of our translation of Herbrand’s unification algorithm in Note 150 with the translation in [Herbrand, 1971].

With regard to logicians, however, notwithstanding our above critique, the elaborately commented book [Herbrand, 1971] is a great achievement and still the best source on Herbrand as a logician (cf. Note 50), and our lectures would not have been possible without Heijenoort’s most outstanding and invaluable contributions to this subject. To the best of our knowledge, what we called Heijenoort’s correction of Herbrand’s False Lemma has not been published before, and we have included it into our version of Herbrand’s Fundamental Theorem. The consequences of this correction on Herbrand’s Modus Ponens elimination (as described in § 13) are most relevant still today and should become part of the standard knowledge on logic, just as Gentzen’s Cut elimination.

While Herbrand’s important work on decidability and consistency of arithmetic was soon to be topped by Presburger and Gentzen, his Fundamental Theorem will remain of outstanding historical and practical significance. Even under the critical assumptions (cf. the discussion in § 14) that Herbrand took the outer Skolemized form from [Skolem, 1928] and that he had realized that the presentation in [Löwenheim, 1915] included a sound and complete proof procedure, Herbrand’s Fundamental Theorem remains a truly remarkable creation.

All in all, Jacques Herbrand has well deserved to be the idol that he actually is. And thus we were surprised to find out how little is known on his personality and life, and that there does not seem to be anything like a Herbrand memorial or museum, nor even a street named after him, nor a decent photo of him available in the Internet.^{151} Moreover, a careful bilingual edition of Herbrand’s complete works on the basis of the elaborate previous editorial achievements is in high demand.^{152} Figure 2: Photo of Jacques Herbrand on the expedition during which he found his death.

151The best photo of Herbrand currently to be found in the Internet seems to be the one of Figure 2.

Outside mathematics, Google hits on Herbrand typically refer to P. Herbrand & Cie., a historical street-car production company in Cologne; or else to Herbrand Street close to Russell Square in London, probably named after Herbrand Arthur Russell, the 11^{th} Duke of Bedford.

152Cf. also Note 50.

Acknowledgements

We would like to thank Irving H. Anellis, Paolo Bussotti, and Lawrence C. Paulson — the second readers of our previous handbook article [Wirth &al., 2009] on the same subject — for their numerous, extensive, deep, and most valuable and helpful suggestions for improvement of previous versions of this paper. As always, the second readers are, of course, not responsible for the remaining weaknesses.

Furthermore, we would like to thank John W. Dawson Jr., Christian G. Fermüller, Bernhard Gramlich, Andreas Hallmann, Georg Ch. Moser, Peter Roquette, Andrea Sattler-Klein, James T. Smith, and Magdalena Wolska for substantial help.

Bibliography of Jacques Herbrand

To the best of our knowledge, the following bibliography of Jacques Herbrand (Jr.) is complete, with the exception of his letters in [Gödel, 1986ff., Vol. V, pp. 3–25] and [Roquette, 2009].

Note that for labels of the form [Herbrand …], we have maintained the standard labeling as introduced by Jean van Heijenoort in [Herbrand, 1968; 1971] and [Heijenoort, 1971a] as far as appropriate. For instance, Herbrand’s thesis is cited as [Herbrand, 1930] and not as [Herbrand, 1930a], which is in general preferable due to the additional redundancy.

Joint Publications of Jacques Herbrand

[Herbrand & Chevalley, 1931] Jacques Herbrand and Claude Chevalley. Nouvelle démonstration du théorème d’existence en théorie du corps de classes. Comptes rendus hebdomadaires des séances de l’Académie des Sciences (Paris), 193:814–815, 1931.

Publications of Jacques Herbrand as Single Author

[Herbrand, 1928] Jacques Herbrand. Sur la théorie de la démonstration. Comptes rendus hebdomadaires des séances de l’Académie des Sciences (Paris), 186:1274–1276, 1928. Also in [Herbrand, 1968, pp. 21–23]. Annotated English translation On Proof Theory by Warren Goldfarb with an extended note by Burton Dreben and Goldfarb in [Herbrand, 1971, pp. 29–34].

[Herbrand, 1929] Jacques Herbrand. Non-contradiction des axiomes arithmétiques. Comptes rendus hebdomadaires des séances de l’Académie des Sciences (Paris), 188:303– 304, 1929. Also in [Herbrand, 1968, pp. 25–26]. Annotated English translation The Consistency of the Axioms of Arithmetic by Warren Goldfarb in [Herbrand, 1971, pp. 35–37]. (An abstract of [Herbrand, 1930, Chapter 4]).

[Herbrand, 1929a] Jacques Herbrand. Sur quelques propriétés des propositions vraies et leurs applications. Comptes rendus hebdomadaires des séances de l’Académie des Sciences (Paris), 188:1076–1078, 1929. Also in [Herbrand, 1968, pp. 27–29]. Annotated English translation On several properties of true propositions and their applications by Warren Goldfarb in [Herbrand, 1971, pp. 38–40]. (An abstract of [Herbrand, 1930, Chapter 5, § 6]).

[Herbrand, 1929b] Jacques Herbrand. Sur le probléme fondamental des mathématiques. Comptes rendus hebdomadaires des séances de l’Académie des Sciences (Paris), 189:554– 556, 1929. Also in [Herbrand, 1968, pp. 31–33]. Annotated English translation On the Fundamental Problem of Mathematics by Warren Goldfarb in [Herbrand, 1971, pp. 41– 43]. (An abstract of [Herbrand, 1931]).

[Herbrand, 1930] Jacques Herbrand. Recherches sur la Théorie de la Démonstration. PhD thesis, Université de Paris, 1930. Thèses présentées à la faculté des Sciences de Paris pour obtenir le grade de docteur ès sciences mathématiques — 1^{re} thèse: Recherches sur la théorie de la démonstration — 2^{me} thèse: Propositions données par la faculté, Les équations de Fredholm — Soutenues le 1930 devant la commission d’examen — Président: M. Vessiot, Examinateurs: MM. Denjoy, Frechet — Vu et approuvé, Paris, le 20 Juin 1929, Le doyen de la faculté des Sciences, C. Maurain — Vu et permis d’imprimer, Paris, le 20 Juin 1929, Le recteur de l’Academie de Paris, S. Charlety — No. d’ordre 2121, Série A, No. de Série 1252 — Imprimerie J. Dziewulski, Varsovie — Univ. de Paris. Also in Prace Towarzystwa Naukowego Warszawskiego, Wydział III Nauk Matematyczno-Fizychnych, Nr. 33, Warszawa. Also in [Herbrand, 1968, pp. 35–153]. Annotated English translation Investigations in Proof Theory by Warren Goldfarb (Chapters 1–4) and Burton Dreben and Jean van Heijenoort (Chapter 5) with a brief introduction by Goldfarb and extended notes by Goldfarb (Notes A–C, K–M, O), Dreben (Notes F–I), Dreben and Goldfarb (Notes D, J, and N), and Dreben, George Huff, and Theodore Hailperin (Note E) in [Herbrand, 1971, pp. 44–202]. English translation of § 5 with a different introduction by Heijenoort and some additional extended notes by Dreben also in [Heijenoort, 1971a, pp. 525–581]. (Herbrand’s PhD thesis, his cardinal work, dated April 14, 1929; submitted at the Univ. of Paris; defended at the Sorbonne June 11, 1930; printed in Warsaw, 1930.)

[Herbrand, 1930a] Jacques Herbrand. Les bases de la logique hilbertienne. Revue de Métaphysique et de Morale, 37:243–255, 1930. Also in [Herbrand, 1968, pp. 155–166]. Annotated English translation The Principles of Hilbert’s Logic in [Herbrand, 1971, pp. 203– 214]. (Herbrand’s personal view on meta-mathematics and Hilbert’s programme).

[Herbrand, 1930b] Jacques Herbrand. Nouvelle démonstration et généralisation d’un théorème de Minkowski. Comptes rendus hebdomadaires des séances de l’Académie des Sciences (Paris), 191:1282–1285, 1930.

[Herbrand, 1931] Jacques Herbrand. Sur le problème fondamental de la logique mathématique. Revue de Métaphysique et de Morale, 24:12–56, 1931. Also in [Herbrand, 1968, pp. 167–207]. Annotated English translation On the Fundamental Problem of Mathematical Logic in [Herbrand, 1971, pp. 215–271].

[Herbrand, 1931a] Jacques Herbrand. Note non signeé sur [Herbrand, 1930]. Annales de l’Université de Paris, 6:186–189, 1931. Also in [Herbrand, 1968, pp. 209–214]. English translation Unsigned Note on Herbrand’s Thesis written by Herbrand himself in [Herbrand, 1971, pp. 272–276]. (The philosophy of metamathematics in the Hilbert school (roughly following [Hilbert, 1928]) and the positioning of [Herbrand, 1930] in it are sketched for non-experts).

[Herbrand, 1931b] Inconsistent label replaced with [Herbrand, 1931d] or [Herbrand, 1932a].

[Herbrand, 1931c] Inconsistent label replaced with [Herbrand, 1932a].

[Herbrand, 1931d] Jacques Herbrand. Notice pour Jacques Hadamard. 1931. In [Herbrand, 1968, pp. 215–219]. With annotations and a brief introduction by Jean van Heijenoort. English translation Note for Jacques Hadamard by Warren Goldfarb in [Herbrand, 1971, pp. 277–281]. (Abstracts for non-experts of Herbrand’s mathematical contributions addressed to his presenter to the Academy of Sciences).

[Herbrand, 1931e] Jacques Herbrand. Sur la théorie des corps de nombres de degré infini. Comptes rendus hebdomadaires des séances de l’Académie des Sciences (Paris), 193:594, 1931. (Abstract of [Herbrand, 1932d; 1933]).

[Herbrand, 1931f] Jacques Herbrand. Sur la théorie des groupes de décomposition, d’inertie et de ramication. J. de Math. Pures et Appliquées (J. Liouville), 9:481–498, 1931.

[Herbrand, 1932a] Jacques Herbrand. Sur la non-contradiction de l’Arithmetique. J. für die reine und angewandte Mathematik (Crellesches J.), 166:1–8, 1932. Received July 27, 1931. Without Hasse’s obituary also in [Herbrand, 1968, pp. 221–232]. Annotated English translation On the Consistency of Arithmetic in [Heijenoort, 1971a, pp. 618–628]. Annotated English translation also in [Herbrand, 1971], pp. 282–298. (Consistency of arithmetic, foreshadowing of (total) recursive functions, discussion of [Gödel, 1931]).

[Herbrand, 1932b] Jacques Herbrand. Sur les classes des corps circulaires. J. de Math. Pures et Appliquées (J. Liouville), 9:417–441, 1932.

[Herbrand, 1932c] Jacques Herbrand. Sur les théorèmes du genre principal et des idéaux principaux. Abhandlungen aus dem mathematischen Seminar der Univ. Hamburg, 9:84– 92, 1932.

[Herbrand, 1932d] Jacques Herbrand. Théorie arithmétique des corps de nombres de degré infini — I. Extensions algébriques finies de corps infinis. Mathematische Annalen, 106:473–501, 1932.

[Herbrand, 1932e] Jacques Herbrand. Une propriété du discriminant des corps algébriques. Annales Scientifiques d l’École Normale Supérieure, 49:105–112, 1932.

[Herbrand, 1932f] Jacques Herbrand. Zur Theorie der algebraischen Funktionen. Mathematische Annalen, 106:502, 1932.

[Herbrand, 1933] Jacques Herbrand. Théorie arithmétique des corps de nombres de degré infini — II. Extensions algébriques de degré infini. Mathematische Annalen, 108:699–717, 1933. Ed. and with a last paragraph by Claude Chevalley.

[Herbrand, 1936] Jacques Herbrand. Le Développement Moderne de la Théorie des Corps Algébriques — Corps de classes et lois de réciprocité. Mémorial des Sciences Mathématiques, Fascicule LXXV. Gauthier-Villars, Paris, 1936. Ed. and with an appendix by Claude Chevalley.

[Herbrand, 1968] Jacques Herbrand. Écrits Logiques. Presses Universitaires de France, Paris, 1968. Ed. by Jean van Heijenoort. English translation is [Herbrand, 1971].

[Herbrand, 1971] Jacques Herbrand. Logical Writings. Harvard Univ. Press, 1971. Ed. by Warren Goldfarb. Translation of [Herbrand, 1968] with additional annotations, brief introductions, and extended notes by Goldfarb, Burton Dreben, and Jean van Heijenoort. (Still the best source on Herbrand’s logical writings today).

References

[Ackermann, 1925] Wilhelm Ackermann. Begründung des ’tertium non datur‘ mittels der Hilbertschen Theorie der Widerspruchsfreiheit. Mathematische Zeitschrift, 93:1–36, 1925. Received March 30, 1924.

[Ackermann, 1928] Wilhelm Ackermann. Über die Erfüllbarkeit gewisser Zählausdrücke. Mathematische Annalen, 100:638–649, 1928. Received Feb. 9, 1928.

[Ackermann, 1940] Wilhelm Ackermann. Zur Widerspruchsfreiheit der Zahlentheorie. Mathematische Annalen, 117:163–194, 1940. Received Aug. 15, 1939.

[Andrews, 2002] Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press (Elsevier), 2002. 2^{nd} ed. (1^{st} ed. 1986).

[Andrews, 2003] Peter B. Andrews. Herbrand Award acceptance speech. J. Automated Reasoning, 31:169– 187, 2003.

[Anellis, 1991] Irving H. Anellis. The Löwenheim–Skolem Theorem, theories of quantification, and proof theory. 1991. In [Drucker, 1991, pp. 71–83].

[Anellis, 1992] Irving H. Anellis. Logic and Its History in the Work and Writings of Jean van Heijenoort. Modern Logic Publ., Ames (IA), 1992.

[Anellis, 2006] Irving H. Anellis. Gödel and the naming of Skolem functions. In Sovremennaja logika: problemy teorii, istorii i primenenija v nauke. Materialy IX Obshcherossijskoj nauchnoj konferencii. Sankt-Peterburg, June 22–24, 2006, pages 410–413. Izdatelśtvo Sankt Peterburgskogo Universiteta, St. Peterburg, 2006. ISBN 5-288-03998-4.

[Anon, 1905] Anon, editor. Verhandlungen des Dritten Internationalen Mathematiker-Kongresses, Heidelberg, Aug. 8–13, 1904. Verlag von B. G. Teubner, Leipzig, 1905.

[Artin & Schreier, 1927] Emil Artin and Otto Schreier. Algebraische Konstruktion reeller Körper. Abhandlungen aus dem mathematischen Seminar der Univ. Hamburg, 5:85–99, 1927. Hamburg, Mathematisches Seminar, June 1926. Facsimile also in [Artin, 1965, pp. 258–272].

[Artin, 1927] Emil Artin. Über die Zerlegung definiter Funktionen in Quadrate. Abhandlungen aus dem mathematischen Seminar der Univ. Hamburg, 5:100–115, 1927. Hamburg, Mathematisches Seminar, June 1926. Facsimile also in [Artin, 1965, pp. 273–288].

[Artin, 1965] Emil Artin. Collected Papers. Addison-Wesley, 1965. Ed. by Serge Lang and John T. Tate. Reprinted 1982 by Springer.

[Autexier, 2005] Serge Autexier. The core calculus. In 20^{th} Int. Conf. on Automated Deduction, Tallinn, 2005, number 3632 in Lecture Notes in Artificial Intelligence, pages 84–98. Springer, 2005.

[Baaz & Fermüller, 1995] Matthias Baaz and Christian G. Fermüller. Non-elementary speedups between different versions of tableaux. In Int. Conf. on Tableaus and Related Methods, TABLEAUX’95, number 918 in Lecture Notes in Artificial Intelligence, pages 217–230. Springer, 1995.

[Baaz & Leitsch, 1995] Matthias Baaz and Alexander Leitsch. Methods of functional extension. Collegium Logicum — Annals of the Kurt Gödel Society, 1:87–122, 1995.

[Badesa, 2004] Calixto Badesa. The Birth of Model Theory — Löwenheim’s Theorem in the Frame of the Theory of Relatives. Princeton Univ. Press, 2004. Translated by Michaël Maudsley.

[Behmann, 1922] Heinrich Behmann. Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem. Mathematische Annalen, 86:163–229, 1922.

[Berka & Kreiser, 1973] Karel Berka and Lothar Kreiser, editors. Logik-Texte – Kommentierte Auswahl zur Geschichte der modernen Logik. Akademie-Verlag, Berlin, 1973. 2^{nd} rev. ed. (1^{st} ed. 1971; 4^{th} rev. rev. ed. 1986).

[Bernays & Schönfinkel, 1928] Paul Bernays and Moses Schönfinkel. Zum Entscheidungsproblem der mathematischen Logik. Mathematische Annalen, 99:342–372, 1928.

[Bernays, 1928] Paul Bernays. Zusatz zu Hilberts Vortrag ”Die Grundlagen der Mathematik“ . Abhandlungen aus dem mathematischen Seminar der Univ. Hamburg, 6:89–92, 1928. English translation On the Consistency of Arithmetic in [Heijenoort, 1971a, pp. 485–489].

[Bitbol & Gayon, 2006] Michel Bitbol and Jean Gayon, editors. L’épistémologie française, 1830–1970. Presses Universitaires de France, Paris, 2006.

[Bourbaki, 1939ff.] Nicolas Bourbaki. Théorie des Ensembles. Éléments des Mathématique. Hermann, Paris, 1939ff..

[Brady, 2000] Geraldine Brady. From Peirce to Skolem: A Neglected Chapter in the History of Logic. North-Holland (Elsevier), 2000.

[Brouwer, 1925a] Luitzen Brouwer. Zur Begründung der intutionistischen Mathematik I. Mathematische Annalen, 93:244–257, 1925.

[Brouwer, 1925b] Luitzen Brouwer. Zur Begründung der intutionistischen Mathematik II. Mathematische Annalen, 95:453–472, 1925.

[Brouwer, 1926] Luitzen Brouwer. Zur Begründung der intutionistischen Mathematik III. Mathematische Annalen, 96:451–488, 1926.

[Cantor, 1932] Georg Cantor. Gesammelte Abhandlungen mathematischen und philosophischen Inhalts. Springer, 1932. Ed. by Ernst Zermelo, reprinted by Georg Olms Verlag, Hildesheim, 1962.

[Cartwright, 1965] Mary L. Cartwright. Jacques Hadamard (1865–1963). Biographical Memoirs of Fellows of the Royal Society, 11:75–99, 1965.

[Chang & Lee, 1973] Chin-Liang Chang and Richard Char-Tung Lee. Symbolic logic and mechanical theorem proving. Academic Press (Elsevier), 1973.

[Chevalley & Lautman, 1931] Claude Chevalley and Albert Lautman. Notice biographique sur Herbrand. Annuaire de l’Association amicale de secours des anciens élèves de l’École Normale Supérieure, 1931:13– 15, 1931. Also in [Herbrand, 1968, pp. 13–15]. English translation Biographical Note on Herbrand in [Herbrand, 1971, pp. 25–28].

[Chevalley, 1935] Claude Chevalley. Sur la pensée de Jacques Herbrand. L’Enseignement Mathématique, 34:97–102, 1935. Also in [Herbrand, 1968, pp. 17–20]. English translation On Herbrand’s Thought in [Herbrand, 1971, pp. 25–28].

[Chevalley, 1982] Claude Chevalley. Jacques Herbrand. 1982. In [Stern, 1982, pp. 1–2].

[Craig, 1957a] William Craig. Linear reasoning — a new form of the Herbrand–Gentzen Theorem. J. Symbolic Logic, 22:250–268, 1957.

[Craig, 1957b] William Craig. Three uses of the Herbrand–Gentzen Theorem in relating model theory and proof theory. J. Symbolic Logic, 22:269–285, 1957.

[Dalen, 1974] Dirk van Dalen. Review: Jacques Herbrand: Logical writings by Warren Goldfarb. The Journal of Philosophy, 71:544–549, 1974.

[Davis & Putnam, 1960] Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. of the ACM, 7:201–215, 1960.

[Davis, 1963] Martin Davis. Eliminating the irrelevant from mechanical proofs. In Proceedings of Symposia in Applied Mathematics, volume 15, pages 15–30, 1963. Also in [Siekmann & Wrightson, 1983, Vol. 1, pp. 315–330].

[Dawson Jr., 1991] John W. Dawson Jr. The reception of Gödel’s incompleteness theorems. 1991. In [Drucker, 1991, pp. 84–100].

[Dawson Jr., 1993] John W. Dawson Jr. Prelude to recursion theory: the Gödel–Herbrand correspondence. 1993. In [Wołkowski, 1993, pp. 1–13].

[Delzell, 1996] Charles N. Delzell. Kreisel’s unwinding of Artin’s proof. 1996. In [Odifreddi, 1996, pp. 113– 246].

[Dieudonné, 1982] Jean Dieudonné. Jacques Herbrand et la théorie des nombres. 1982. In [Stern, 1982, pp. 3–7].

[Dieudonné, 1999] Jean Dieudonné. Claude Chevalley. Transformation Groups, 4:103–113, 1999. Dedicated to the memory of Claude Chevalley.

[Dreben & Denton, 1963] Burton Dreben and John Denton. A supplement to Herbrand. J. Symbolic Logic, 31(3):393–398, 1963.

[Dreben & Denton, 1970] Burton Dreben and John Denton. Herbrand-style consistency proofs. 1970. In [Myhill &al., 1970, pp. 419–433].

[Dreben &al., 1963] Burton Dreben, Peter B. Andrews, and Stål Aanderaa. False lemmas in Herbrand. Bull. American Math. Soc., 69:699–706, 1963.

[Drucker, 1991] Thomas Drucker, editor. Perspectives on the History of Mathematical Logic. Birkhäuser (Springer), 1991.

[Dubreil, 1983] Paul Dubreil. Souvenirs d’un boursier Rockefeller 1929–1931. Cahiers du séminaire d’histoire des mathématiques, 4:61–73, 1983.

[Dubucs & Égré, 2006] Jacques Dubucs and Paul Égré. Jacques Herbrand. 2006. In [Bitbol & Gayon, 2006, pp. 301–322].

[Enderton, 1972] Herbert B. Enderton. A Mathematical Introduction to Logic. Academic Press (Elsevier), 1972.

[Feferman, 1996] Sol(omon) Feferman. Kreisel’s “unwinding” program. 1996. In [Odifreddi, 1996, pp. 247– 273].

[Feigenbaum & Feldman, 1963] Edward A. Feigenbaum and J. Feldman, editors. Computers and Thought. McGraw-Hill, 1963.

[Forster, 1997] Thomas E. Forster. Quine’s NF—60 years on. American Mathematical Monthly, 104:838– 845, 1997.

[Frege, 1879] Gottlob Frege. Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Verlag von L. Nebert, Halle an der Saale, 1879. Corrected facsimile in [Frege, 1964]. Reprint of pp. III–VIII and pp. 1–54 in [Berka & Kreiser, 1973, pp. 48–106]. English translation in [Heijenoort, 1971a, pp. 1–82].

[Frege, 1884] Gottlob Frege. Die Grundlagen der Arithmetik. Verlag von M. & H. Marcus, Breslau, 1884. Reprinted 1934. Reprinted as facsimile: Georg Olms Verlag, Hildesheim, 1990.

[Frege, 1893/1903] Gottlob Frege. Grundgesetze der Arithmetik – Begriffsschriftlich abgeleitet. Verlag von Hermann Pohle, Jena, 1893/1903. As facsimile with corrigenda by Christian Thiel: Georg Olms Verlag, Hildesheim, 1998.

[Frege, 1964] Gottlob Frege. Begriffsschrift und andere Aufsätze. Wissenschaftliche Buchgesellschaft, Darmstadt, 1964. Zweite Auflage, mit Edmund Husserls und Heinrich Scholz’ Anmerkungen, herausgegeben von Ignacio Angelelli.

[Gabbay & Woods, 2004ff.] Dov Gabbay and John Woods, editors. Handbook of the History of Logic. Elsevier, 2004ff..

[Gentzen, 1935] Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935. Also in [Berka & Kreiser, 1973, pp. 192–253]. English translation in [Gentzen, 1969].

[Gentzen, 1936] Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112:493–565, 1936. English translation in [Gentzen, 1969].

[Gentzen, 1938] Gerhard Gentzen. Die gegenwärtige Lage in der mathematischen Grundlagenforschung – Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, Neue Folge, 4:3–44, 1938. Reprinted as facsimile by Wissenschaftliche Buchgesellschaft, Darmstadt, Verlag von S. Hirzel, Stuttgart. English translation in [Gentzen, 1969].

[Gentzen, 1943] Gerhard Gentzen. Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie. Mathematische Annalen, 119:140–161, 1943. Received July 9, 1942. English translation in [Gentzen, 1969].

[Gentzen, 1969] Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. North-Holland (Elsevier), 1969. Ed. by Manfred E. Szabo.

[Gilmore, 1960] Paul C. Gilmore. A proof method for quantification theory: Its justification and realization. IBM Journal Research and Development, 4:28–35, 1960. Also in [Siekmann & Wrightson, 1983, Vol. I, pp. 151–161].

[Gödel, 1930] Kurt Gödel. Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik und Physik, 37:349–360, 1930. With English translation also in [Gödel, 1986ff., Vol. I, pp. 102–123].

[Gödel, 1931] Kurt Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173–198, 1931. With English translation also in [Gödel, 1986ff., Vol. I, pp. 145–195]. English translation also in [Heijenoort, 1971a, pp. 596–616].

[Gödel, 1934] Kurt Gödel. On Undecidable Propositions of Formal Mathematical Systems. The Inst. for Advanced Study, 1934. Lecture notes by Stephen C. Kleene and Barkley Rosser. With English translation also in [Gödel, 1986ff., Vol. I, pp. 346–372].

[Gödel, 1939] Kurt Gödel. Consistency proof for the generalized continuum hypothesis. In Proc. of the National Academy of Sciences, U.S.A., 25, pages 220–224, 1939. Also in [Gödel, 1986ff., Vol. II, pp. 28– 32].

[Gödel, 1986ff.] Kurt Gödel. Collected Works. Oxford Univ. Press, 1986ff. Ed. by Sol(omon) Feferman, John W. Dawson Jr., Jean van Heijenoort, Stephen C. Kleene, &al..

[Goldfarb & Scanlon Jr., 1974] Warren Goldfarb and Thomas M. Scanlon Jr. The ω-consistency of number theory via Herbrand’s theorem. J. Symbolic Logic, 39:678–692, 1974.

[Goldfarb, 1993] Warren Goldfarb. Herbrand’s error and Gödel’s correction. Modern Logic, 3:103–118, 1993.

[Gonseth, 1941] Ferdinand Gonseth, editor. Les Entretiens de Zurich sur les Fondements et la Méthode des Sciences Mathématiques, Dec. 6–9, 1938. S. A. Leemann frères & Cie., Zürich, 1941.

[Gove, 1993] Philipp Babcock Gove, editor. Webster’s Third New International Dictionary. Merriam-Webster, Springfield (MA), 1993. Principal copyright 1961.

[Hadamard, 1949] Jacques S. Hadamard. The Psychology of Invention in the Mathematical Field. Princeton Univ. Press, 1949. 2^{nd} rev. ed. (1^{st} ed. 1945).

[Hasse & Herbrand Sr., 1931] Helmut Hasse and Jacques Herbrand Sr.. Letters exchanged between Helmut Hasse and Jacques Herbrand Sr.. Available from the Niedersächsische Staats- und Universitätsbibliothek – Abteilung für Handschriften und seltene Drucke, Göttingen, Germany, 1931.

[Heijenoort, 1968] Jean van Heijenoort. On the relation between the falsifiability tree method and the Herbrand method in quantification theory. Unpublished typescript, Nov. 20, 1968, 12 pp.; Jean van Heijenoort Papers, 1946–1988, Archives of American Mathematics, Center for American History, Univ. of Texas at Austin, Box 3.8/86-33/1. Copy in Anellis Archives, 1968.

[Heijenoort, 1971a] Jean van Heijenoort. From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931. Harvard Univ. Press, 1971. 2^{nd} rev. ed. (1^{st} ed. 1967).

[Heijenoort, 1971b] Jean van Heijenoort. Reviews of articles by Grigori Mints. J. Symbolic Logic, 36:524– 528, 1971.

[Heijenoort, 1975] Jean van Heijenoort. Herbrand. Unpublished typescript, May 18, 1975, 15 pp.; Jean van Heijenoort Papers, 1946–1988, Archives of American Mathematics, Center for American History, Univ. of Texas at Austin, Box 3.8/86-33/1. Copy in Anellis Archives, 1975.

[Heijenoort, 1982] Jean van Heijenoort. L’œuvre logique de Herbrand et son contexte historique. 1982. In [Stern, 1982, pp. 57–85].

[Heijenoort, 1986a] Jean van Heijenoort. Absolutism and relativism in logic. 1986. In [Heijenoort, 1986b, pp. 75–83].

[Heijenoort, 1986b] Jean van Heijenoort. Selected Essays. Bibliopolis, Napoli, copyright 1985. Also published by Librairie Philosophique J. Vrin, Paris, 1986, 1986.

[Heijenoort, 1986c] Jean van Heijenoort. Herbrand’s work in logic and its historical context. 1986. In [Heijenoort, 1986b, pp. 99–121].

[Herbrand …, …] Please search for labels on Herbrand in the bibliography preceeding this list of references!

[Heyting, 1930a] Arend Heyting. Die formalen Regeln der intuitionistischen Logik. Sitzungsberichte der Preußischen Akademie der Wissenschaften, Berlin, Physikalisch-mathematische Klasse II, 1930:42–56, 1930. Short version also in [Berka & Kreiser, 1973], pp. 173–178.

[Heyting, 1930b] Arend Heyting. Die formalen Regeln der intuitionistischen Mathematik. Sitzungsberichte der Preußischen Akademie der Wissenschaften, Berlin, Physikalisch-mathematische Klasse II, 1930:57– 71, 158–169, 1930.

[Heyting, 1971] Arend Heyting. Intuitionism — An Introduction. North-Holland (Elsevier), 1971. 3^{rd} rev. ed. (1^{st} ed. 1956).

[Hilbert & Ackermann, 1928] David Hilbert and Wilhelm Ackermann. Grundzüge der theoretischen Logik. Springer, 1928.

[Hilbert & Bernays, 1968/70] David Hilbert and Paul Bernays. Die Grundlagen der Mathematik. Springer, 1968/70. 2^{nd} rev. ed. (1^{st} ed. 1934/39).

[Hilbert, 1899] David Hilbert. Grundlagen der Geometrie. Verlag von B. G. Teubner, Leipzig, 1899. In Festschrift zur Feier der Enthüllung des Gauß-Weber-Denkmals in Göttingen, herausgegeben von dem Fest-Comitee. 1^{st} ed. without appendixes. Last edition by Hilbert is [Hilbert, 1930a], which is also most complete regarding the appendixes. Last three editions by Paul Bernays are [Hilbert, 1962; 1968; 1972], which are also most complete regarding supplements and figures. Two substantially different English translations are [Hilbert, 1902] and [Hilbert, 1971].

[Hilbert, 1900] David Hilbert. Über den Zahlbegriff. Jahresbericht der Deutschen Mathematiker-Vereinigung, 8:180–184, 1900. Reprinted as Appendix VI of [Hilbert, 1909; 1913; 1922a; 1923; 1930a].

[Hilbert, 1902] David Hilbert. The Foundations of Geometry. Open Court, Chicago, 1902. Authorized English translation of [Hilbert, 1899] by E. J. Townsend.

[Hilbert, 1903] David Hilbert. Grundlagen der Geometrie. Zweite, durch Zusätze vermehrte und mit fünf Anhängen versehene Auflage. Mit zahlreichen in den Text gedruckten Figuren. Druck und Verlag von B. G. Teubner, Leipzig, 1903. 2^{nd} rev. extd. ed. of [Hilbert, 1899], rev. and extd. with five appendixes, newly added figures, and an index of notion names.

[Hilbert, 1905] David Hilbert. Über die Grundlagen der Logik und der Arithmetik. 1905. In [Anon, 1905, 174–185]. Reprinted as Appendix VII of [Hilbert, 1909; 1913; 1922a; 1923; 1930a]. English translation On the foundations of logic and arithmetic by Beverly Woodward with an introduction by Jean van Heijenoort in [Heijenoort, 1971a, pp. 129–138].

[Hilbert, 1909] David Hilbert. Grundlagen der Geometrie. Dritte, durch Zusätze und Literaturhinweise von neuem vermehrte und mit sieben Anhängen versehene Auflage. Mit zahlreichen in den Text gedruckten Figuren. Druck und Verlag von B. G. Teubner, Leipzig, Berlin, 1909. 3^{rd} rev. extd. ed. of [Hilbert, 1899], rev. ed. of [Hilbert, 1903], extd. with a bibliography and two additional appendixes (now seven in total) (Appendix VI: [Hilbert, 1900]) (Appendix VII: [Hilbert, 1905]).

[Hilbert, 1913] David Hilbert. Grundlagen der Geometrie. Vierte, durch Zusätze und Literaturhinweise von neuem vermehrte und mit sieben Anhängen versehene Auflage. Mit zahlreichen in den Text gedruckten Figuren. Druck und Verlag von B. G. Teubner, Leipzig, Berlin, 1913. 4^{th} rev. extd. ed. of [Hilbert, 1899], rev. ed. of [Hilbert, 1909].

[Hilbert, 1922a] David Hilbert. Grundlagen der Geometrie. Fünfte, durch Zusätze und Literaturhinweise von neuem vermehrte und mit sieben Anhängen versehene Auflage. Mit zahlreichen in den Text gedruckten Figuren. Verlag und Druck von B. G. Teubner, Leipzig, Berlin, 1922. 5^{th} extd. ed. of [Hilbert, 1899]. Contrary to what the sub-title says, this is an anastatic reprint of [Hilbert, 1913], extended with a very short preface on the changes w.r.t. [Hilbert, 1913], and with augmentations to Appendix II, Appendix III, and Chapter IV, § 21.

[Hilbert, 1922b] David Hilbert. Neubegründung der Mathematik (Erste Mitteilung). Abhandlungen aus dem mathematischen Seminar der Univ. Hamburg, 1:157–177, 1922. Reprinted with notes in [Hilbert, 1932ff., Vol. 3, pp. 157–177].

[Hilbert, 1923] David Hilbert. Grundlagen der Geometrie. Sechste unveränderte Auflage. Anastatischer Nachdruck. Mit zahlreichen in den Text gedruckten Figuren. Verlag und Druck von B. G. Teubner, Leipzig, Berlin, 1923. 6^{th} rev. extd. ed. of [Hilbert, 1899], anastatic reprint of [Hilbert, 1922a].

[Hilbert, 1926] David Hilbert. Über das Unendliche. Mathematische Annalen, 88:151–165, 1926. Received June 24, 1925. Reprinted as Appendix VIII of [Hilbert, 1930a]. English translation On the infinite by Stefan Bauer-Mengelberg with an introduction by Jean van Heijenoort in [Heijenoort, 1971a, pp. 367– 392].

[Hilbert, 1928] David Hilbert. Die Grundlagen der Mathematik – Vortrag, gehalten auf Einladung des Mathematischen Seminars im Juli 1927 in Hamburg. Abhandlungen aus dem mathematischen Seminar der Univ. Hamburg, 6:65–85, 1928. Reprinted as Appendix IX of [Hilbert, 1930a]. English translation The foundations of mathematics by Stefan Bauer-Mengelberg and Dagfinn Føllesdal with a short introduction by Jean van Heijenoort in [Heijenoort, 1971a, pp. 464–479].

[Hilbert, 1930a] David Hilbert. Grundlagen der Geometrie. Siebente umgearbeitete und vermehrte Auflage. Mit 100 in den Text gedruckten Figuren. Verlag und Druck von B. G. Teubner, Leipzig, Berlin, 1930. 7^{th} rev. extd. ed. of [Hilbert, 1899], thoroughly revised edition of [Hilbert, 1923], extd. with three new appendixes (now ten in total) (Appendix VIII: [Hilbert, 1926]) (Appendix IX: [Hilbert, 1928]) (Appendix X: [Hilbert, 1930b]).

[Hilbert, 1930b] David Hilbert. Probleme der Grundlegung der Mathematik. Mathematische Annalen, 102:1–9, 1930. Vortrag gehalten auf dem Internationalen Mathematiker-Kongreß in Bologna, Sept. 3, 1928. Received March 25, 1929. Reprinted as Appendix X of [Hilbert, 1930a]. Short version in Atti del congresso internationale dei matematici, Bologna, 3–10 settembre 1928, Vol. 1, pp. 135–141, Bologna, 1929.

[Hilbert, 1931] David Hilbert. Die Grundlegung der elementaren Zahlenlehre. Mathematische Annalen, 104:485–494, 1931.

[Hilbert, 1932ff.] David Hilbert. Gesammelte Abhandlungen. Springer, 1932ff..

[Hilbert, 1956] David Hilbert. Grundlagen der Geometrie. Achte Auflage, mit Revisionen und Ergänzungen von Dr. Paul Bernays. Mit 124 Abbildungen. B. G. Teubner Verlagsgesellschaft, Stuttgart, 1956. 8^{th} rev. extd. ed. of [Hilbert, 1899], rev. ed. of [Hilbert, 1930a], omitting appendixes VI–X, extd. by Paul Bernays, now with 24 additional figures and 3 additional supplements.

[Hilbert, 1962] David Hilbert. Grundlagen der Geometrie. Neunte Auflage, revidiert und ergänzt von Dr. Paul Bernays. Mit 129 Abbildungen. B. G. Teubner Verlagsgesellschaft, Stuttgart, 1962. 9^{th} rev. extd. ed. of [Hilbert, 1899], rev. ed. of [Hilbert, 1956], extd. by Paul Bernays, now with 129 figures, 5 appendixes, and 8 supplements (I 1, I 2, II, III, IV 1, IV 2, V 1, V 2).

[Hilbert, 1968] David Hilbert. Grundlagen der Geometrie. Zehnte Auflage, revidiert und ergänzt von Dr. Paul Bernays. Mit 124 Abbildungen. B. G. Teubner Verlagsgesellschaft, Stuttgart, 1968. 10^{th} rev. extd. ed. of [Hilbert, 1899], rev. ed. of [Hilbert, 1962] by Paul Bernays.

[Hilbert, 1971] David Hilbert. The Foundations of Geometry. Open Court, Chicago and La Salle (IL), 1971. Newly translated and fundamentally different 2^{nd} ed. of [Hilbert, 1902], actually an English translation of [Hilbert, 1968] by Leo Unger.

[Hilbert, 1972] David Hilbert. Grundlagen der Geometrie. 11. Auflage. Mit Supplementen von Dr. Paul Bernays. B. G. Teubner Verlagsgesellschaft, Stuttgart, 1972. 11^{th} rev. extd. ed. of [Hilbert, 1899], rev. ed. of [Hilbert, 1968] by Paul Bernays.

[Hintikka, 1996] K. Jaakko J. Hintikka. The Principles of Mathematics Revisited. Cambridge Univ. Press, 1996.

[Howard & Rubin, 1998] Paul Howard and Jean E. Rubin. Consequences of the Axiom of Choice. American Math. Society, 1998.

[Kant, 1781] Immanuël Kant. Critik der reinen Vernunft. Johann Friedrich Hartknoch, Riga, 1781. 1^{st} ed..

[Kant, 1787] Immanuël Kant. Critik der reinen Vernunft. Johann Friedrich Hartknoch, Riga, 1787. 2^{nd} rev. ed. of [Kant, 1781].

[Kleene, 1938] Stephen Cole Kleene. On notation for ordinal numbers. J. Symbolic Logic, 3(150–155), 1938.

[Kleene, 1952] Stephen Cole Kleene. Introduction to Metamathematics. North-Holland (Elsevier), 1952.

[Kreisel, 1951] Georg Kreisel. On the interpretation of non-finitist proofs — Part I. J. Symbolic Logic, 16:241–267, 1951.

[Kreisel, 1952] Georg Kreisel. On the interpretation of non-finitist proofs — Part II. J. Symbolic Logic, 17:43–58, iv, 1952.

[Kreisel, 1958] Georg Kreisel. Mathematical significance of consistency proofs. J. Symbolic Logic, 23:155– 182, 1958.

[Kreisel, 1982] Georg Kreisel. Finiteness theorems in arithmetic: an application of Herbrand’s theorem for Σ_{2}-formulas. 1982. In [Stern, 1982, pp. 39–55].

[Lemmermeyer & Roquette, 2006] Franz Lemmermeyer and Peter Roquette. Helmut Hasse–Emmy Noether — Die Korrespondenz 1925–1935. Universitätsverlag Göttingen, 2006.

[Löwenheim, 1915] Leopold Löwenheim. Über Möglichkeiten im Relativkalkül. Mathematische Annalen, 76:228–251, 1915. English translation On Possibilities in the Calculus of Relatives by Stefan Bauer-Mengelberg with an introduction by Jean van Heijenoort in [Heijenoort, 1971a, pp. 228–251].

[Loveland, 1978] Donald W. Loveland. Automated Theorem Proving: A Logical Basis. North-Holland (Elsevier), 1978.

[Marchisotto & Smith, 2007] Elena Anne Marchisotto and James T. Smith. The Legacy of Mario Pieri in Geometry and Arithmetic. Birkhäuser (Springer), 2007.

[Miller, 1992] Dale A. Miller. Unification under a mixed prefix. J. Symbolic Computation, 14(321–358), 1992.

[Moore, 1987] Gregory H. Moore. A house divided against itself: The emergence of first-order logic as the basis for mathematics. 1987. In [Phillips, 1987, pp. 98–136].

[Myhill &al., 1970] John Myhill, Akiko Kino, and Richard Vesley, editors. Intuitionism and Proof Theory. Proceedings of the International Conference Intuitionism and Proof Theory, Buffalo, 1968. North-Holland (Elsevier), 1970.

[Neumann, 1925] John von Neumann. Eine Axiomatisierung der Mengenlehre. J. für die reine und angewandte Mathematik (Crellesches J.), 154:219–240, 1925. Correction in [Neumann, 1926]. English translation An Axiomatization of Set Theory by Stefan Bauer-Mengelberg with an introduction by Jean van Heijenoort in [Heijenoort, 1971a, pp. 393–413].

[Neumann, 1926] John von Neumann. Berichtigung zu der Arbeit ”Eine Axiomatisierung der Mengenlehre“ . J. für die reine und angewandte Mathematik (Crellesches J.), 155:128, 1926. Correction of [Neumann, 1925].

[Neumann, 1927] John von Neumann. Zur Hilbertschen Beweistheorie. Mathematische Zeitschrift, 26:1– 46, 1927. Received July 29, 1925. (First occurrence of the notion of basic typus (Grundtypus), the cardinal notion in the theory of ε-substitution. Clarification that the consitency proof of [Ackermann, 1925] does not include second order with comprehension.)

[Neumann, 1928] John von Neumann. Die Axiomatisierung der Mengenlehre. Mathematische Zeitschrift, 27(669–752), 1928.

[Newell &al., 1957] Allen Newell, J. C. Shaw, and Herbert A. Simon. Empirical explorations with the Logic Theory Machine: A case study in heuristics. In Proc. Western Joint Computer Conf., pages 218–230. The Institute of Radio Engineers, New York, 1957. Also in [Feigenbaum & Feldman, 1963, pp. 109–133]. Also in [Siekmann & Wrightson, 1983, Vol. I, pp. 49–73].

[Nicod, 1917] Jean Nicod. A reduction in the number of primitive propositions of logic. Proc. Cambridge Philosophical Soc., 19:32–44, 1917.

[Nonnengart, 1996] Andreas Nonnengart. Strong skolemization. Research Report MPI-I-96-2-010, Max-Planck-Institut für Informatik, Im Stadtwald, D–66123 Saarbrücken, 1996.

[Odifreddi, 1996] Piergiorgio Odifreddi, editor. Kreiseliana — About and Around Georg Kreisel. A K Peters, Wellesley (MA), 1996.

[Parsons, 1998] Charles Parsons. Finitism and intuitive knowledge. 1998. In [Schirn, 1998, pp. 249–270].

[Peckhaus, 2004] Volker Peckhaus. Schröder’s logic. 2004. In [Gabbay & Woods, 2004ff., Vol. 3: The Rise of Modern Logic: From Leibniz to Frege, pp. 557–610].

[Peirce, 1885] Charles S. Peirce. On the algebra of logic: A contribution to the philosophy of notation. American J. of Mathematics, 7:180–202, 1885. Also in [Peirce, 1993, pp. 162–190].

[Peirce, 1993] Charles S. Peirce. Writings of Charles S. Peirce — A Chronological Edition, Vol. 5, 1884– 1886. Indiana Univ. Press, 1993. Ed. by Christian J. W. Kloesel.

[Phillips, 1987] Esther R. Phillips, editor. Studies in the History of Mathematics. Mathematics Association of America, Washington (DC), 1987.

[Pieri, 1907/8] Mario Pieri. Sopra gli assiomi aritmetici. Il Bollettino delle seduta della Accademia Gioenia di Scienze Naturali in Catania, Series 2, 1–2:26–30, 1907/8. English translation On the Axioms of Arithmetic in [Marchisotto & Smith, 2007, § 4.2, pp. 308–313].

[Presburger, 1930] Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Sprawozdanie z I Kongresu metematyków krajów słowianskich, Warszawa 1929, (Comptes-rendus du 1^{re} Congrès des Mathématiciens des Pays Slaves, Varsovie 1929), pages 92–101+395, 1930. Remarks and English translation: [Stanisfer, 1984].

[Reid, 1970] Constance Reid. Hilbert. Springer, 1970.

[Ribet, 1976] Kenneth A. Ribet. A modular construction of unramified p-extensions of Q(μp). Inventiones mathematicae, 34:151–162, 1976.

[Robinson & Voronkow, 2001] Alan Robinson and Andrei Voronkow, editors. Handbook of Automated Reasoning. Elsevier, 2001.

[Robinson, 1965] J. Alan Robinson. A machine-oriented logic based on the resolution principle. J. of the ACM, 12:23–41, 1965. Also in [Siekmann & Wrightson, 1983, Vol. 1, pp. 397–415].

[Roquette, 2000] Peter Roquette. On the history of Artins L-functions and conductors — seven letters from Artin to Hasse in the year 1930. Mitteilungen der Mathematischen Gesellschaft in Hamburg, 19:5–50, 2000. Web version updated July 23, 2003.

[Roquette, 2007] Peter Roquette. The correspondence Helmut Hasse–Jacques Herbrand. Personal e-mail communications with Peter Roquette. Cf. also [Roquette, 2009], 2007.

[Roquette, 2009] Peter Roquette, editor. Helmut Hasse–Jacques Herbrand — The complete correspondence, including the six letters of Herbrand to Hasse, dated from May 11 to July 23, 1931, and a letter from Joseph H. M. Wedderburn to Hasse on Herbrand’s planned visit to Princeton, dated May 25, 1931. 2009. To appear

[Rosser, 1936] J. Barkley Rosser. Extensions of some theorems of Gödel and Church. J. Symbolic Logic, 1:87–91, 1936.

[Rubin & Rubin, 1985] Herman Rubin and Jean E. Rubin. Equivalents of the Axiom of Choice. North-Holland (Elsevier), 1985. 2^{nd} rev. ed. (1^{st} ed. 1963).

[Scanlon Jr., 1973] Thomas M. Scanlon Jr. The consistency of number theory via Herbrand’s Theorem. J. Symbolic Logic, 38:29–58, 1973.

[Schirn, 1998] Matthias Schirn, editor. The Philosophy of Mathematics Today. Oxford Univ. Press, 1998.

[Schröder, 1895] Ernst Schröder. Vorlesungen über die Algebra der Logik, Vol. 3, Algebra der Logik und der Relative, Vorlesungen I-XII. B. G. Teubner Verlagsgesellschaft, Leipzig, 1895. English translation of some parts in [Brady, 2000].

[Schütte, 1960] Kurt Schütte. Beweistheorie. Springer, 1960.

[Sieg, 2005] Wilfried Sieg. Only two letters: The correspondence between Herbrand and Gödel. The Bulletin of Symbolic Logic, 11(2):172–184, 2005.

[Siekmann & Wrightson, 1983] Jörg Siekmann and Graham Wrightson, editors. Automation of Reasoning. Springer, 1983.

[Siekmann, 1989] Jörg Siekmann. Unification theory. J. Symbolic Logic, 7:207–274, 1989.

[Skolem, 1919] Thoralf Skolem. Untersuchungen über die Axiome des Klassenkalküls und über Produktations- und Summationsprobleme, welche gewisse Klassen von Aussagen betreffen. Skrifter, Norske Videnskaps-Akademi i Oslo (= Videnskapsselskapet i Kristiania), Matematisk-Naturvidenskapelig Klasse, J. Dybwad, Oslo, 1919/3:1–37, 1919. Dated May 26, 1917. Also in [Skolem, 1970, pp. 67–101]. (First explicit occurrence of quantifier elimination).

[Skolem, 1920] Thoralf Skolem. Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischer Sätze nebst einem Theorem über dichte Mengen. Skrifter, Norske Videnskaps-Akademi i Oslo (= Videnskapsselskapet i Kristiania), Matematisk-Naturvidenskapelig Klasse, J. Dybwad, Oslo, 1920/4:1–36, 1920. Also in [Skolem, 1970, pp. 103–136]. English translation of § 1 Logico-Combinatorial Investigations in the Satisfiability or Provability of Mathematical Propositions: A simplified proof of a theorem by Leopold Löwenheim and generalizations of the theorem by Stefan Bauer-Mengelberg with an introduction by Jean van Heijenoort in [Heijenoort, 1971a, pp. 252–263]. (Löwenheim–Skolem Theorem via Skolem normal form and choice of a sub-model).

[Skolem, 1923a] Thoralf Skolem. Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichem Ausdehnungsbereich. Skrifter, Norske Videnskaps-Akademi i Oslo (= Videnskapsselskapet i Kristiania), Matematisk-Naturvidenskapelig Klasse, J. Dybwad, Oslo, 1923/6:1–38, 1923. Written 1919. Also in [Skolem, 1970, pp. 153–188]. English translation The foundations of elementary arithmetic established by means of the recursive mode of thought, without the use of apparent variables ranging over infinite domains by Stefan Bauer-Mengelberg with an introduction by Jean van Heijenoort in [Heijenoort, 1971a, pp. 302–333].

[Skolem, 1923b] Thoralf Skolem. Einige Bemerkungen zur axiomatischen Begründung der Mengenlehre. In Proc. 5^{th} Scandinaviska Matematikerkongressen, Helsingfors, July 4–7, 1922, pages 217–232, Helsingfors, 1923. Akademiska Bokhandeln. Also in [Skolem, 1970, pp. 137–152]. English translation Some remarks on Axiomatized Set Theory by Stefan Bauer-Mengelberg with an introduction by Jean van Heijenoort in [Heijenoort, 1971a, pp. 290–301]. (The best written and, together with [Skolem, 1920], the most relevant publication on the Löwenheim–Skolem Theorem; although there is some minor gap in the proof according to Wang [1970], cured in [Skolem, 1929]. Includes Skolem’s Paradox and a proof of the Löwenheim– Skolem Theorem which does not require any weak forms of the Axiom of Choice, via Skolem normal form and construction of a model without assuming the previous existence of another one).

[Skolem, 1928] Thoralf Skolem. Über die mathematische Logik (Nach einem Vortrag gehalten im Norwegischen Mathematischen Verein am 22. Oktober 1928). Nordisk Matematisk Tidskrift, 10:125–142, 1928. Also in [Skolem, 1970, pp. 189–206]. English translation On Mathematical Logic by Stefan Bauer-Mengelberg and Dagfinn Føllesdal with an introduction by Burton Dreben and Jean van Heijenoort in [Heijenoort, 1971a, pp. 508–524]. (First explicit occurrence of Skolemization and Skolem functions).

[Skolem, 1929] Thoralf Skolem. Über einige Grundlagenfragen der Mathematik. Skrifter, Norske Videnskaps-Akademi i Oslo (= Videnskapsselskapet i Kristiania), Matematisk-Naturvidenskapelig Klasse, J. Dybwad, Oslo, 1929/4:1–49, 1929. Also in [Skolem, 1970, pp. 227–273]. (Detailed discussion of Skolem’s Paradox and the Löwenheim–Skolem Theorem).

[Skolem, 1941] Thoralf Skolem. Sur la portée du théorème de Löwenheim–Skolem. 1941. In [Gonseth, 1941, pp. 25–52]. Also in [Skolem, 1970, pp. 455–482].

[Skolem, 1970] Thoralf Skolem. Selected Works in Logic. Universitetsforlaget Oslo, 1970. Ed. by Jens E. Fenstad. (Without index, but with most funny spellings in the newly set titles).

[Smullyan, 1968] Raymond M. Smullyan. First-Order Logic. Springer, 1968.

[Stanisfer, 1984] Ryan Stanisfer. Presburger’s Article on Integer Arithmetic: Remarks and Translation. Dept. of Computer Science, Cornell Univ., Ithaca, NY, 1984.

[Stern, 1982] Jacques Stern, editor. Proc. of the Herbrand Symposium, Logic Colloquium’81, Marseilles, France, July 1981. North-Holland (Elsevier), 1982.

[Tait, 1981] William W. Tait. Finitism. J. of Philosophy, 78:524–546, 1981.

[Tait, 2006] William W. Tait. Gödel’s correspondence on proof theory and constructive mathematics. Philosophia Mathematica (III), 14:76–111, 2006.

[Tarski, 1951] Alfred Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley and Los Angeles, 1951. 2^{nd} rev. ed. (1^{st} ed.: Rand Corporation, Santa Monica (CA), 1948).

[Vihan, 1995] Přemysl Vihan. The last months of Gerhard Gentzen in Prague. Collegium Logicum — Annals of the Kurt Gödel Society, 1:1–7, 1995.

[Wallen, 1990] Lincoln A. Wallen. Automated Proof Search in Non-Classical Logics. MIT Press, 1990.

[Wang, 1970] Hao Wang. A survey of Skolem’s work in logic. In [Skolem, 1970], pages 17–52, 1970.

[Weyl, 1921] Hermann Weyl. Über die neue Grundlagenkrise der Mathematik. Mathematische Zeitschrift, 14:39–79, 1921.

[Weyl, 1928] Hermann Weyl. Diskussionsbemerkungen zu dem zweiten Hilbertschen Vortrag über die Grundlagen der Mathematik. Abhandlungen aus dem mathematischen Seminar der Univ. Hamburg, 6:86–88, 1928.

[Whitehead & Russell, 1910–1913] Alfred North Whitehead and Bertrand Russell. Principia Mathematica. Cambridge Univ. Press, 1910–1913. 1^{st} ed. (2^{nd} rev. ed. 1925ff.).

[Wirth &al., 2009] Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller, and Serge Autexier. Jacques Herbrand: Logic, life, and automated deduction. 2009. In [Gabbay & Woods, 2004ff., Vol. 5: Logic from

Russell to Church]. http://www.ags.uni-sb.de/~cp/p/herbrand.

[Wirth, 2004] Claus-Peter Wirth. Descente Infinie + Deduction. Logic J. of the IGPL, 12:1–96, 2004.

http://www.ags.uni-sb.de/~cp/p/d.

[Wirth, 2006] Claus-Peter Wirth. lim+, δ^{+}, and Non-Permutability of β-Steps. SEKI-Report SR–2005–01 (ISSN 1437–4447). SEKI Publications, Saarland Univ., 2006. rev. ed. of July 30, 2006. http://www.ags.

uni-sb.de/~cp/p/nonpermut.

[Wirth, 2008] Claus-Peter Wirth. Hilbert’s epsilon as an operator of indefinite committed choice. J.

Applied Logic, 6:287–317, 2008. http://www.ags.uni-sb.de/~cp/p/epsi, http://dx.doi.org/10.
1016/j.jal.2007.07.009.

[Wirth, 2009] Claus-Peter Wirth. Shallow confluence of conditional term rewriting systems. J. Symbolic

Computation, 44:69–98, 2009. http://www.ags.uni-sb.de/~cp/p/shallow, http://dx.doi.org/10.
1016/j.jsc.2008.05.005.

[Wittgenstein, 1939] Ludwig Wittgenstein. Lectures on the Foundations of Mathematics, Cambridge. Univ. of Chicago Press, copyright 1989, 1939. Cora Diamond (ed.), from the notes of R. G. Bosanquet, Norman Malcolm, Rush Rhees, and Yorick Smythies.

[Wołkowski, 1993] Zbigniew Wołkowski, editor. 1^{st} Int. Symposium on Gödel’s Theorem, Paris, May 27–29, 1991. World Scientific Publishing, 1993.

[Zach, 2001] Richard Zach. Hilbert’s Finitism: Historical, Philosophical, and Metamathematical Perspectives. PhD thesis, Univ. of California, Berkeley, 2001.

[Zaremba, 1926] Stanisław Zaremba. La Logique des Mathématiques. Mémorial des Sciences Mathématiques, Fascicule XV. Gauthier-Villars, Paris, 1926.

[Zygmunt, 1991] Jan Zygmunt. Mojżesz Presburger: Life and work. History and Philosophy of Logic, 12:211–223, 1991.

66

Index

A^{T}, 21 T_{n}, 20

Ackermann, Wilhelm, 5, 14, 18, 37, 42, 55,

59, 62 α, 22 Andrews, Peter B., 18, 29, 40, 55, 57 Anellis

Archives, 59

Irving H., 4, 22, 27, 37, 40, 50, 55 anti-prenex, see direction, anti-prenex and form,

anti-prenex Artin

’s Theorem, 7, 55

Artin’s proof, 7, 57 Emil, 6, 7, 10, 18, 55, 63

Autexier, Serge, 1, 35 axiom

of choice, 22, 26, 35–39

weak forms, see Principle of Dependent

Choice, König’s Lemma of infinity, 18 of reducibility, 18 of substitutability, 40

axioms Dedekind–Peano, 40 of equality, 40, 42

Bauer-Mengelberg, Stefan, 12–14, 38, 60, 62,

64 Benzmüller, Christoph, 1 Bernays, Paul, 4, 10, 14, 18, 24, 25, 28–29,

31, 33, 38, 41, 42, 56, 59 β, 22 Brouwer, Luitzen, 12, 16, 44, 56 Bussotti, Paolo, 50

champ fini, 5, 20, 26, 31–32

definition, 20 Chevalley

Catherine, 9

Claude, 9, 16, 18, 51, 54, 56, 57 Church, Alonzo, 29, 63 completeness, 14, 18, 37–40

definition, 14 consistency, 12–14

of arithmetic, 4–5, 14, 40–42, 44 of first-order logic, 11, 37 proof of, 4–5, 14, 40–42, 44

Gentzen’s, see Gentzen’s consistency

proof Herbrand-style, see Herbrand-style

consistency proof contentual

history of the English word, 13 correction (of Herbrand’s False Lemma) Gödel’s and Dreben’s, 29, 32

definition, 29 Heijenoort’s, 29, 31, 32, 34, 35

definition, 29 Courant, Richard, 10 Craig

’s Interpolation Theorem, 5 William, 5, 56

Cut elimination, 5, 15, 32, 35, 49

Dalen, Dirk van, 4, 56

Davis –Putnam procedure, 47 Martin, 46–47, 56

Dawson, John W., Jr., 11, 44, 50, 56–58 Dedekind, see also axioms, Dedekind–Peano

Richard, 12 deep, see inference, deep δ, 22

-quantifier, see quantifier, δ- -variable, see variable, δ-

Dieudonné, Jean, 9, 18, 57

direction

anti-prenex, 26 definition, 25

prenex, 25

definition, 25 Dreben, Burton, 5, 15, 22, 29, 51, 52, 54, 57,

64

elimination, see Modus Ponens elimination, Cut elimination

Feferman, Sol(omon), 4, 7, 57, 58

Fermüller, Christian G., 23, 26, 29, 50, 55 finitism, 11–14, 16–18, 35–39, 44 form

anti-prenex, 28 definition, 25 functional, 22 prenex, 20, 28, 29, 31, 32, 34, 39

definition, 25 Skolem normal, 39 (outer) Skolemized, 22, 23, 26–29, 32, 38,

39 definition, 23 example, 22 vs. Skolem normal form, 39

inner Skolemized, 23, 29

definition, 23 Forster, Thomas E., 11, 57 Frege, Gottlob, 11–13, 17, 21, 27, 57 function

index, 22 indicial, 22 recursive, 4–5, 41–44 Skolem, 22–23

γ, 22 -quantifier, see quantifier, γ- -variable, see variable, γ-

Generalized Rule

of δ-Quantification, 25, 31–34

definition, 25 of γ-Quantification, 24, 29, 31–34

definition, 24 of γ-Simplification, 25, 31–33

definition, 25 of Simplification, 25, 26, 29, 31, 35

definition, 25 Gentzen

’s calculi, 4, 15, 35 ’s consistency proof, 5, 42 ’s Hauptsatz, 5, 15, 32, 35 ’s verschärfter Hauptsatz, 35 Gerhard, 3–5, 14, 15, 22, 42, 58, 65

Gilmore, Paul C., 46 Gödel

’s Completeness Theorem, 37–39 ’s First Incompleteness Theorem, 11, 14 ’s Second Incompleteness Theorem, 5, 11,

14, 42, 44 ’s and Dreben’s correction, see correction Kurt, 5, 9–11, 15, 16, 18, 22, 28, 37–39,

42–44, 51, 53, 57, 58, 63 Göttingen, 10, 18 Goldfarb, Warren, 5, 15, 19, 22, 29, 39, 51,

52, 54, 56, 58 Gramlich, Bernhard, 50

Hadamard, Jacques S., 9–10, 20, 56, 59 Hallmann, Andreas, 50 Hasse, Helmut, 6, 10, 15, 18, 59, 62, 63 height of a term, 20, 23, 27, 28, 34, 35

definition, 20

treatment of the lexicon, 28 Heijenoort

’s correction, see correction

Jean van, 12–19, 25–29, 31, 32, 35, 37–39,

44, 51–53, 55–60, 62, 64 Herbrand

’s False Lemma, 20, 28–29, 31, see also

correction definition, 28

’s Fundamental Theorem, 4–5, 15, 20, 24,

26, 28–37, 45 definition, 31 application, 42 –Ribet Theorem, 6–7 -style consistency proof, 5 complexity, 26–27 definition, 26 example, 27

disjunction, 26–33, 45–46 definition, 26 example, 27

expansion, 20–21, 26, 27, 32 definition, 21 example, 21 Jacques, 3–64 Jacques, Sr. (Herbrand’s father), 9–10, 59 universe, 20, 45–47 definition, 20 Heyting, Arend, 15–16, 59 Hilbert

’s epsilon, 4, 5, 27, 29, 33, 35, 42, 63, 65 ’s finitism, see finitism ’s programme, see programme, Hilbert’s -style calculi, 34, see also Hilbert, school,

calculi of David, 4, 6, 10, 12–14, 16–18, 24, 25, 27, 28, 31, 33, 37, 39, 41, 42, 52, 56, 59– 62

school, 4, 16–19, 24, 35, 37, 42 calculi of, 24, 31

identity, see also tautology

normal, 26

definition, 26 inference

deep, 19, 25, 31, 35

rules of, see Rule infinite

the actual, 14, 16 intuitionism, 12, 15–16, 44, see also finitism

and logic, intuitionistic

Kant, Immanuël, 13–14, 61 König’s Lemma, 38–39 Kreisel, Georg, 4, 57, 61, 62 Kronecker, Leopold, 6, 16

Löwenheim

–Skolem Theorem, 4, 17, 26, 31, 35–39 à la [Skolem, 1923b], 39 à la Löwenheim [1915], 37

–Skolem–Tarski Theorem

Upward, 40 Leopold, 11, 17, 21, 26, 27, 29–30, 35–39,

49, 62, 69 Lautman, Albert, 9, 56 logic

classical, 11 first-order, 17 intuitionistic, 15, 16, see also intuition-

ism machine-oriented, 47 two-valued, 11

modus ponens, 5, 15, 24, 29, 31–35 definition, 24 elimination, 5, 15, 29, 32–35, 49

Moser, Georg Ch., 50

Neumann, John von, 10, 18, 39, 42, 44, 62 Nicod, Jean, 18, 62 Noether, Emmy, 6, 10, 62 notation

uniform, 21–22

paradox, see Russell’s Paradox and Skolem’s

Paradox Paulson, Lawrence C., 50 Peano, see also axioms, Dedekind–Peano

Guiseppe, 12, 17 Peckhaus, Volker, 17, 63 Peirce

–Schröder tradition, 17, 27, 40 –Schröder tradition, 38 Charles S., 12, 17, 19, 21, 27, 56, 63

Poincaré, Henri, 16 prenex, see direction, prenex and form,

prenex Presburger

Arithmetic, 41, 46 Mojżesz, 41, 63–65

Principia Mathematica, 12, 17, 24, 31, 65

calculi of, 24, 31 Principle of Dependent Choice, 38 programme

Fifth Generation Computer, 48 Hilbert’s, 4–5, 12–14, 16–18, 42 unwinding, 4–7

proof search, 34–35, 45–47 automatic, 34, 45–47 human-oriented, 34

Property A, 17, 26, 29, 31, 35

definition, 26 Property B, 26

definition, 26 Property C, 5, 26–32, 35–37, 39, 42, 45

definition, 26 example, 27

quantifier δ-, 23 γ-, 23 general, 23 restricted, 23

raising, 39 Robinson, J. Alan, 45, 47, 63 Roquette, Peter, 9, 10, 15, 18, 50, 51, 62, 63 Rule, see also Generalized Rule

of δ-Quantification, 31

definition, 25 of γ-Quantification, 31, 34

definition, 25 of Generalization, 25 of Implication, 25 of Passage, 25, 26, 28, 29, 31, 35

definition, 25 of Simplification, 25, 29, 31, 33

definition, 25 Russell, see also Principia Mathematica

’s Paradox, 11, 12, 14, 18 Bertrand, 12, 17, 18, 24, 27, 31, 39, 65

Sattler-Klein, Andrea, 50 Scanlon, Thomas M., Jr., 5, 22, 42, 58, 63 Schröder, see also Peirce-Schröder tradition

Ernst, 12, 17, 21, 27, 63 sentential tautology, see tautology, sentential Sieg, Wilfried, 5, 43, 64 Siekmann, Jörg, 1, 47, 56, 58, 62–64 Skolem, see also form, Skolem normal and

form, Skolemized and function, Skolem and Löwenheim–Skolem Theorem and Löwenheim–Skolem– Tarksi Theorem and Skolemization and term, Skolem

’s Paradox, 39

Thoralf, 17, 21, 26, 27, 30, 37–40, 46, 49,

64, 65, 69 Skolemization, 21–22 Smith, James T., 50, 62, 63 Smullyan

’s uniform notation, see notation, uni-

form Raymond M., 22, 64

A^{T}, 21 T_{n}, 20 Tait, William W., 16, 29, 65 Tarski, Alfred, 11, 41, 65 tautology

sentential, 24

substitutional sentential, 24 term

Skolem, 21–23 theorem proving

automated, 34, 43–47 human-oriented, 34, 43, 44 inductive, 43, 44

unification algorithm, 47–48 uniform notation, see notation, uniform

variable bound δ-, 23

bound γ-, 23
free δ-, 23
free γ-, 23

Vessiot, Ernest, 9–10

Wang, Hao, 38–40, 64, 65 Wedderburn, Joseph H. M., 10, 63 Weil, André, 9, 18 Weyl, Hermann, 12, 16, 65 Whitehead, see also Principia Mathematica

Alfred North, 12 Wirth, Claus-Peter, 1, 23, 27, 34, 35, 40, 44,

50, 65 Wittgenstein, Ludwig, 11, 65 Wolska, Magdalena, 50 Zaremba, Stanisław, 17, 65