Herbrand’s Fundamental Theorem

Claus-Peter Wirth

FB AI, Hochschule Harz, 38855 Wernigerode, Germany

First submission May 24, 2014 Revised Aug. 14, 2014

— to appear in the Internet Encyclopedia of Philosophy —

Abstract

Herbrand’s Fundamental Theorem provides a constructive characterization of derivability in first-order predicate logic by means of sentential logic.

Sometimes it is simply called “Herbrand’s Theorem”, but the longer name is preferable as there are other important “Herbrand theorems” and Herbrand himself called it “Théorème fondamental”.

It was ranked by Bernays [1957] as follows: “In its proof-theoretic form, Herbrand’s Theorem can be seen as the central theorem of predicate logic. It expresses the relation of predicate logic to propositional logic in a concise and felicitous form.” And by Heijenoort [1967]: “Let me say simply, in conclusion, that Begriffsschrift [Frege, 1879], Löwenheim’s paper [1915], and Chapter 5 of Herbrand’s thesis [1930] are the three cornerstones of modern logic.”

Herbrand’s Fundamental Theorem occurs in Chapter 5 of his PhD thesis [1930]

— entitled Recherches sur la théorie de la démonstration — submitted by Jacques Herbrand (1908–1931) in 1929 at the University of Paris.

Herbrand’s Fundamental Theorem is, together with Gödel’s incompleteness theorems and Gentzen’s Hauptsatz, one of the most influential theorems of modern logic.

Because of its complexity, Herbrand’s Fundamental Theorem is typically fouled up in textbooks beyond all recognition. As we are convinced that there is still much more to learn for the future from this theorem than many logicians know, we will focus on the true message and its practical impact. This requires a certain amount of streamlining of Herbrand’s work, which will be compensated by some remarks on the actual historical facts.

Contents

1 Informal Introduction 3 1.1 Validity in Sentential and in First-Order Logic . . . . . . . . . . . . . . . 3 1.2 Calculi: Soundness, Completeness, Decidability . . . . . . . . . . . . . . 4 1.3 First Major Aspect of Herbrand’s Fundamental Theorem . . . . . . . . 5 1.4 Second Major Aspect of Herbrand’s Fundamental Theorem . . . . . . 5 1.5 Also a Completeness Theorem for First-Order Logic . . . . . . . . . . . . 5 1.6 Constructiveness of Herbrand’s Fundamental Theorem . . . . . . . . . 6

2 Formal Presentation 7 2.1 Basic Notions and Notation . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 A Modern Version of Herbrand’s Modus Ponens-Free Calculus . . . . . 8

2.3 Property C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.4 The Theorem and its Lemmas . . . . . . . . . . . . . . . . . . . . . . . . 11

3 Conclusion 12

Acknowledgments 12

References 12

1 Informal Introduction

1.1 Validity in Sentential and in First-Order Logic

The language of classical (i.e. two-valued) sentential logic (also called “propositional logic”) is formed by Boolean operator symbols

— say conjunction ∧, disjunction ∨, negation ¬ —

on sentential variables (i.e. nullary predicate symbols). For simplicity, but without loss of generality, we will consider exactly the three mentioned operators symbols as part of our language of sentential logic in this article. Other operators will be considered just as syntactical sugar; for instance, material implication A⇒B will be considered a metalevel notion defined as ¬A∨B. The interpretation of the Boolean operator symbols is fixed, whereas the sentential variables range over the Boolean values TRUE and FALSE. A sentential formula is valid if it evaluates to TRUE for all interpretations (i.e. mappings to Boolean values) of the sentential variables.

In a first step, let us now add non-nullary predicate symbols, which take terms as arguments. Terms are formed from function symbols and variables over a non-empty domain of individuals, which has to be chosen by any interpretation and is a assumed to be welldetermined and fixed in advance, although it may be infinite. Such a quantifier-free firstorder formula is valid if it evaluates to TRUE for all interpretations of predicate symbols as functions from individuals to Boolean values, of function symbols as functions from individuals to individuals, and of variables as individuals.

Note that this extension is not a substantial one, however, because the notion of validity does not change when we interpret the quantifier-free first-order formulas as sentential formulas, simply by considering the predicates together with their argument terms just as names for atomic sentential variables.

In a second step, we can add quantifiers such as “∀ ” (“for all … ”) and “∃ ” (“there is a … ”) to bind variables. This means that formulas are now formed not only by applying Boolean operators to formulas, but also the singulary operators “∀x.” and ∃x.”, binding an arbitrary variable symbol x. Evaluation is now defined for these additional formula formations in the obvious way: ∃x. A (or else: ∀x. A) evaluates to TRUE if the single formula argument A (its scope) evaluates to TRUE for some interpretation of x (or else: for all interpretations of x); otherwise it evaluates to FALSE.

With this second step we arrive at first-order predicate logic (with function symbols). This logic is crucially different from sentential logic, because the testing of all domains of individuals becomes now unavoidable for determining validity of a formula in general. Even though it actually suffices to check only one domain for each cardinality (different from 0, but including infinite ones), this cannot be executed effectively in general. As noted above, however, the domains do not matter if no quantifiers occur in a first-order formula.

Definition 1.1 (Sentential Validity) A first-order formula is sententially valid if it is quantifier-free and valid in sentential logic, provided that we consider the predicates together with their argument terms just as names for atomic sentential variables. □

Note that a formula does not change its meaning if we replace a bound variable with a fresh one. For instance, there is not difference in validity between

∀x. ( Human(x) ⇒ Mortal(x) )

and ∀y. ( Human(y) ⇒ Mortal(y) ), both expressing that “all humans are mortal” — in a structure where the singulary predicates Human and Mortal have the obviously intended interpretation. Note, however, that none of these equivalent formulas is valid, because we also have to consider the structure where Human is always TRUE and Mortal is FALSE, in which case the formula evaluates to FALSE.

Just like Herbrand, we consider equality of formulas only up to renaming of bound variables. Thus, we consider the two displayed formulas to be identical.

A variable may also occur free in a formula, i.e. not in the scope of any quantifier binding it. We will, however, tacitly consider only formulas where each occurrences of each variable is either free or otherwise bound by a unique quantifier. This excludes ugly formulas such as Human(x)∧∃x.Mortal(x), ∃x.Human(x)∧∃x.Mortal(x), or ∀x.(Human(x)∧∃x.Mortal(x)). The bound variables of such formulas can always be renamed to obtain nicer formulas in our restricted sense, such as Human(x) ∧ ∃z.Mortal(z), ∃x.Human(x) ∧ ∃z.Mortal(z), and ∀x.(Human(x) ∧ ∃z.Mortal(z)). Both human comprehension and formal treatment become less difficult by this common syntactical restriction.

1.2 Calculi: Soundness, Completeness, Decidability

To get a more constructive access to first-order predicate logic, validity has to be replaced with derivability in a calculus. Such a calculus is sound if we can derive only valid formulas with it, and complete if every valid formula can be derived with it. Luckily, there are sound and complete calculi for first-order logic.

Let us consider formal derivation in a sound and complete calculus for first-order logic. Then there are effective enumeration procedures that, in the limit, would produce an infinite list of all derivable consequences. This means that derivability in first-order logic is semidecidable: If we want to find out whether a first-order formula is derivable, we can start such an enumeration procedure and say “yes” if our formula comes along.

Non-derivability in first-order logic, however, is not semi-decidable: There cannot be an enumeration procedure for those first-order formulas which are not derivable. In other words, derivability is not co-semi-decidable.

A problem is decidable if it is both semi- and co-semi-decidable. Therefore, the problem of derivability in first-order logic (historically called the Entscheidungsproblem in engerer Bedeutung, i.e. the decision problem for first-order logic) is not decidable: There cannot be any effective procedure that, for an arbitrary first-order formula as input, always returns an answer “yes” or “no” that is correct w.r.t. its derivability.

Sentential logic, however, is decidable.

Therefore, it makes sense to characterize derivability in first-order logic by a semidecision procedure based on validity in sentential logic.

Remark 1.2 (Historical Correctness) The notion of decidability was developed mainly after Herbrand’s death. The Entscheidungsproblem was an open problem during Herbrand’s lifetime, because the co-semi-undecidability was established only later by Church [1936] and Turing [1936/7]. □

1.3 First Major Aspect of Herbrand’s Fundamental Theorem

A major aspect of Herbrand’s Fundamental Theorem is that it provides a semi-decision procedure for first-order logic as follows: For a given first-order formula A, this procedure produces a list of quantifier-free first-order formulas

F^{T_{1}(F)}, F^{T_{2}(F)}, F^{T_{3}(F)}, …

such that A is derivable in first order-logic if and only if one of the formulas F^{T_{i}(F)} is sententially valid. We say that A has Property C of order i if F^{T_{i}(F)} is sententially valid.

1.4 Second Major Aspect of Herbrand’s Fundamental Theorem

Another major aspect of Herbrand’s Fundamental Theorem is that in Herbrand’s modus ponens-free calculus for first-order logic there is a linear derivation of A from F^{T_{i}(F)}, provided that A has Property C of order i. A derivation is linear if — seen as a tree — it has no branching because all inference rules have exactly one premise. In addition, this derivation also has the so-called “sub”-formula property w.r.t. A. Moreover, contrary to all calculi that were invented before, and similar to the calculi of [Gentzen, 1935], Herbrand’s modus ponens-free calculus gives humans a good chance to actually find this linear derivation based on an informal proof. Furthermore, Herbrand’s modus ponens-free calculus shows a great similarity with today’s approaches to automated theorem proving, greater even than that of the well-known calculi of [Gentzen, 1935].

1.5 Also a Completeness Theorem for First-Order Logic

“Property C” is a name introduced in [Herbrand, 1930]. Without a name, this property occurs already in [Löwenheim, 1915], where it is shown that a first-order formula A is valid if and only if it has Property C of order i, for some positive natural number i — which became famous as the Löwenheim–Skolem Theorem.

In his PhD thesis, Herbrand also showed the equivalence of his own first-order calculi with those of the Hilbert school [Hilbert & Bernays, 2013b] and the Principia Mathematica [Whitehead & Russell, 1910–1913]. Therefore, as a consequence of the Löwenheim–Skolem Theorem, the completeness of all these calculi is an immediate corollary of Herbrand’s Fundamental Theorem.

Herbrand, however, did not trust the notion of first-order validity. As the first follower of Hilbert’s finitistic standpoint in proof theory in France, Herbrand was so radically finitistic that — in the area of logic — he did not accept model theory or set theory at all. And so Gödel proved the completeness of first-order logic first when he submitted his thesis [Gödel, 1930] in 1929, in the same year as Herbrand, and the theorem is now called Gödel’s Completeness Theorem in all textbooks on logic.

Figure: The bridge of the Löwenheim–Skolem Theorem and Herbrand’s Fundamental Theorem, based on the sentential Property C standing firm in the river that divides the banks of valid and derivable formulas in the land of first-order predicate logic.

1.6 Constructiveness of Herbrand’s Fundamental Theorem

Why was the difference between the model-theoretic notion of validity and the constructive notion of derivability in a sound and complete calculus so crucial for Herbrand? The reason, of course, is the undecidability of first-order logic, which essentially requires the non-constructive use of actual infinities in the definition of validity. Hilbert’s program in logic — best described in [Hilbert & Bernays, 2013a] — was to show the consistency of such non-constructive methods in mathematics by finitistic methods, which are even more restrictive than the intuitionistic methods in mathematics following L. E. J. Brouwer.

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, 1986a, p.118]

As a consequence of this “royalist” attitude, Herbrand was very proud on the fact that his Fundamental Theorem is perfectly constructive in the sense that its proof shows how anything claimed can be constructed from anything given: From A, we can construct an arbitrary large part of the sequence F^{T_{1}(F)}, F^{T_{2}(F)}, F^{T_{3}(F)}, …. From a derivation of A, we can compute a number i such that A has Property C of order i (i.e. such that F^{T_{i}(F)} is sententially valid). If A has Property C of order i, we can construct a linear derivation of A from F^{T_{i}(F)} — provided that we are explicitly given i as a definite number.

2 Formal Presentation

2.1 Basic Notions and Notation

Before we can present Herbrand’s Fundamental Theorem formally, we have to provide some further notions and notation on first-order formulas and several inference rules for first-order logic. Note that we will partly use modern notions, which did not exist at Herbrand’s time.

If we want to focus on a certain position in a formula, we write this formula as A[B]. This means that B is a formula that occurs in the context A[…] as a sub-formula at a certain fixed position, which, however, is not explicitly given by the notation. Then we denote with A[C] the formula that results from the formula A[B] by replacing the one occurrence of B at the fixed position with the formula C.

We denote with A{x_{1}↦t_{1}, …, x_{n}↦t_{n}} the result of replacing all occurrences of the distinct variables x_{0}, …, x_{n} in the formula A in parallel with the terms t_{1}, …, t_{n}, respectively. Here, {x_{1}↦t_{1}, …, x_{n}↦t_{n}} is actually a notation for a substitution, i.e. for a function from variables to terms.

The occurrence of a quantifier in a formula is accessible if it is not in the scope of any other quantifier. For instance, in the valid formula

∀x. ∃y. (x ≺ y) ∨ ∃m. ∀z. ¬(m ≺ z)

on the binary predicate symbol ≺ (with infix notation), the occurrences of the quantifiers ∀x. and ∃m. are the only accessible ones. Note that we assume the scopes of our quantifiers to be minimal in the sense that the scope of ∀x. in this formula does not include the subformula ∃m. ∀z. ¬(m ≺ z) — contrary to the formula

∀x. (∃y. (x ≺ y) ∨ ∃m. ∀z. ¬(m ≺ z)),

where only the occurrence of ∀x. is accessible.

Smullyan [1968] classified reductive inference rules — and the inference rules of the Hilbert calculi we will consider here can all be seen as such if we read them bottom up — into α (sentential+non-branching), β (sentential+\underline{b}ranching), γ, and δ. According to this classification, we introduce the following notion on quantifiers, bearing in mind that ∧, ∨, and ¬ are our only Boolean operators.

The occurrence of a quantifier in formula is γ if it is of the form ∃x. and it is in the scope of an even number of negation symbols, or of the form ∀x. and in the scope of an odd number of negation symbols; otherwise the quantifier is δ. (A γ-quantifier turns up as ∃ in a prenex form of the formula, and a δ-quantifier as ∀.)

The occurrence of a variable in a formula is γ if it is bound by a γ-quantifier; it is δ if it is bound by a δ-quantifier or free (i.e. not bound by any quantifier).

2.2 A Modern Version of Herbrand’s Modus Ponens-Free Calculus

Now we are prepared to understand the following three inference rules which constitute a slightly improved version of Herbrand’s modus ponens-free calculus in the style of Heijenoort [1975; 1992; 1986a] and Wirth [2012; 2014].

Note that we may rename bound variables to satisfy the side conditions of the inference rules, because we consider equality of formulas only up to renaming of bound variables.

Generalized rule of γ-quantification: \frac{A[H\{x ↦ t\}]}{A[Qx. H]} where

1. Qx. is an accessible γ-quantifier of A[Qx. H], and

2. the free variables of the term t must not be bound by quantifiers in H.

Example 2.1 (Application of the generalized rule of γ-quantification) If the variable z does not occur free in the term t, we get the following two inference steps with identical premises by application of the generalized rule of γ-quantification at two different positions:

• \begin{matrix}(t ≺ t) & ∨ & ¬∀z. (t ≺ z) \\ (t ≺ t) & ∨ & ∃x. ¬∀z. (x ≺ z) \end{matrix} via the meta-level substitution

{ A[…] ↦ (t ≺ t) ∨ […], H ↦ ¬∀z. (x ≺ z), Q ↦ ∃ };

• \begin{matrix}(t ≺ t) & ∨ & ¬∀z. (t ≺ z) \\ (t ≺ t) & ∨ & ¬∀x. ∀z. (x ≺ z) \end{matrix} via the meta-level substitution

{ A[…] ↦ (t ≺ t) ∨ ¬[…], H ↦ ∀z. (x ≺ z), Q ↦ ∀ }. □

Generalized rule of δ-quantification: \frac{A[H]}{A[Qy. H]} where

1. Qy. is an accessible δ-quantifier of A[Qy. H], and

2. the variable y must not occur free in the context A[…].

Generalized rule of simplification: \frac{A[H ∘ H′]}{A[H]} where

1. “∘” stands for “∨” if […] occurs in the scope of an even number of negation symbols in A[…], and for “∧” otherwise, and

2. H′ is a variant of the sub-formula H (i.e., H′ is H or can be obtained from H by the renaming of variables bound in H).

Moreover, the generalized rule of γ-simplification is the sub-rule for the case that H is of the form Qy. C and Qy. is a γ-quantifier of A[Qy. C].

Remark 2.2 (Historic Version of Herbrand’s Modus Ponens-Free Calculus)

The before-mentioned three rules are to be used for a modern presentation of Herbrand’s modus ponens-free calculus. The historical modus ponens-free calculus of Herbrand actually had the generalized rule of simplification, but only the shallow rules of “γ- and δ-quantification”, compensated by the addition of the rules of passage.

Rules of γ- and δ-quantification result from our formalization of the generalized rules by restricting A[…] to the empty context (i.e. A[Qx. H], e.g., is just Qx. H).

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 (where B is a formula in which the variable x does not occur free):

\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}

Note that Herbrand did not need rules of passage for conjunction (besides the rules of passage for negation (1, 2) and for disjunction (3, 4, 5, 6)), because he considered conjunction A∧B a meta-level notion defined as ¬(¬A ∨¬B).

Herbrand needed his rules of passage (in anti-prenex direction) for the completeness of his historic modus ponens-free calculus because the shallow rules of quantification — contrary to the generalized ones — cannot introduce quantifiers at non-top positions.

Herbrand introduced these rules in § 2.2 of his PhD thesis [Herbrand, 1930]. He named the rules of γ- and δ-quantification “second” and “first rule of generalization” [Herbrand, 1971, p. 74f.], respectively (“deuxième” and “première règle de généralisation” [Herbrand, 1968, p. 68f.]). At the same places, we also find the “rules of passage” (“règles de passage” ). Finally, in § 5.6.A of his PhD Thesis, Herbrand also introduces the generalized rule of simplification [Herbrand, 1971, p. 175] (“règle de simplification généralisée” [Herbrand, 1968, p. 143]). □

2.3 Property C

Definition 2.3 (Height of a Term, Champ Fini T_{n}(F))

We use |t| to denote the height of a term t, which is given by

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

For a positive natural number n and a formula F, 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}(F). The terms of T_{n}(F) are constructed from the symbols that occur free in F: the function symbols, the constant symbols (which we will tacitly subsume under the function symbols in what follows), and the free variable symbols (which can be seen as constant symbols here). Such a champ fini differs from a full term universe in containing only the terms t with |t| ≺ n.

So we have T_{1}(F) = ∅.

To guarantee T_{n}(F) ≠ ∅ for n ≻ 1, in case that neither constants nor free variable symbols occur in F, we will assume that a fresh constant symbol “•” (which does not occur elsewhere) is included in the term construction in addition to the free symbols of F. □

Herbrand’s definition of an expansion follows the traditional idea that — for a finite domain — universal (existential) quantification can be seen as a finite conjunction (disjunction) over the elements of the domain:

Definition 2.4 (Expansion) Let T be a finite set of terms. To simplify substitution, let A be a formula whose bound variables do not occur in T . The expansion A^{T} of A w.r.t. T is the formula given by the following recursive definition. If A is quantifier-free formula, then A^{T} := A. Moreover: (¬A_{1})^{T} := ¬A_{1}^{T},

\begin{aligned}(A_{1} ∨ A_{2})^{T} & := & A_{1}^{T} ∨ A_{2}^{T} , \\ (A_{1} ∧ A_{2})^{T} & := & A_{1}^{T} ∧ A_{2}^{T} , \end{aligned} \begin{aligned}(∃x. A)^{T} & := & ⋁_{t∈T} A^{T} \{x↦t\}, \\ (∀x. A)^{T} & := & ⋀_{t∈T} A^{T} \{x↦t\}. \end{aligned}  □

Definition 2.5 (Outer Skolemized Form) The outer Skolemized form of a formula A results from A by removing every δ-quantifier and replacing its bound variable x with x^{δ}(y_{1}, …, y_{m}), where x^{δ} is a fresh (“Skolem”) symbol and y_{1}, …, y_{m}, in this order, are the variables of the γ-quantifiers in whose scope the δ-quantifier occurs. □

Definition 2.6 (Property C) Let A be a first-order formula. Let n be a positive natural number. Let F be the outer Skolemized form of A. A has Property C of order 1 if F is a sentential tautology. For n > 1, the formula A has Property C of order n if the expansion F^{T_{n}(F)} is a sentential tautology. □

2.4 The Theorem and its Lemmas

Theorem 2.7 (Herbrand’s Fundamental Theorem à la Heijenoort) Let A be a first-order formula. The following two statements are logically equivalent. Moreover, we can construct a witness for each statement from a witness for the other one.

1. There is a positive natural number n such that A has Property C of order n.

2. There is a sentential tautology B, and there is a derivation of A from B that consists in applications of the generalized rules of simplification, δ-quantification, and γ-quantification (and in the renaming of bound variables). □

As we can decide Property C of order n for n = 1, n = 2, n = 3, …, Theorem 2.7 immediately provides us with a semi-decision procedure for derivability (and, thus, by the Löwenheim– Skolem Theorem, also for validity) of any first-order formula A given as input.

Note that the witnesses mentioned in Theorem 2.7 are, of course, on the one hand, a concrete representation of the natural number n, and, on the other hand, concrete representations of the formula B and of the derivation of A from B.

To get some more information on the construction of these witnesses, we have to decompose the equivalence of Theorem 2.7 into the two implications found in the following two lemmas, which constitute the theorem.

Lemma 2.8 (From Property C to a Linear Derivation) Let A be a first-order formula. Let F be the outer Skolemized form of A. Let n be a positive natural number. 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 the sentential tautology F^{T_{n}(F)}.
Step 2: Then we may repeatedly apply the generalized rules of δ- and γ-quantification.
Step 3: Then we may repeatedly apply the generalized rule of γ-simplification.
Step 4: Then we rename all bound δ-variables to obtain A.

□

The proof idea of Lemma 2.8 is to transform the computation of the expansion of the outer Skolemized form into a reduction in Herbrand’s modus ponens-free calculus. In this transformation, Skolemization cannot remove the δ-quantifiers, but just renames bound variables to Skolem terms considered as variable names. The remaining critical task is then to schedule the order of the expansion steps such that the side conditions of the resulting reductive applications of the inference rules are met.

Find an elaborate, but easily conceivable example for the actual construction of such a derivation — which also shows how to deal with the problems of how to overcome the inefficiency of this procedure and how to actually find a proof of a manageable size — in [Wirth, 2014, § 5].

Lemma 2.9 (From a Linear Derivation to Property C) If there is a derivation of the first-order formula A from a sentential tautology by applications of the generalized rules of simplification, and of γ- and δ-quantification (and renaming of bound variables),

then A has Property C of order 1 + ∑_{i=1}^{m} |t_{i}| ,

where t_{1}, …, t_{m} are the instances for the meta-variable t of the generalized rule of γ-quantification in its m applications in the derivation of A. □

Remark 2.10 (Historical Version of Herbrand’s Fundamental Theorem)

As already explained in Remark 2.2, Herbrand’s actual calculus was a bit different and had to take the detour via adding quantifiers on top level and then moving them in. This seemed to admit a minor simplification by a detour via the prenex normal form. To reduce a problem to problems of manageable size (divide et impera), the detour via prenex normal form was a leading standard at Herbrand’s time. Meanwhile prenex normal form plays only a minor rôle in the better logic courses because of its crucial efficiency problems.

In Herbrand’s case this problem turned out to be fatal for the correctness of his proof: Herbrand computed the upper bound for the order of Property C after application of the rules of passage much lower than it actually is. This is well-documented under the name of Herbrand’s “False Lemma”.

One correction of Herbrand’s “False Lemma” is the one that we have presented in this article and that consists in adding — to Herbrand’s deep version of his inference rule of simplification — also the deep versions of his inference rules of quantification. Looking at the style in which the great mathematician Jacques Herbrand organized his most creative work in logic we may say that, if anybody had noticed this bug in Herbrand’s proof during Herbrand’s lifetime, this correction would have been the most straightforward bug fix for him. Moreover, this correction still is the most straightforward and most elegant one today. It was clearly outlined by Jean van Heijenoort, but first sketched in publication in [Wirth &al., 2009], and first published with an explicit presentation in [Wirth, 2012].

3 Conclusion

In this article we have delivered that we consider the very essentials that any logician should know on Herbrand’s Fundamental Theorem, and we suggest [Wirth, 2014] and [Wirth &al., 2014] for further reading on Herbrand’s Fundamental Theorem, Herbrand’s further work in logic, and for a listing of further sources on the subject.

Acknowledgments

I would like to thank Irving H. Anellis (1946–2013) for all his kind help for me and my work on Jacques Herbrand and Jean van Heijenoort. Irving has made my life better and richer. His death has left a gap in my life.

References

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

[Bernays, 1957] Paul Bernays. Über den Zusammenhang des Herbrandschen Satzes mit den neueren Ergebnissen von Schütte und Stenius. In Proceedings of the International Congress of Mathematicians 1954, Groningen and Amsterdam, 1957. Noordhoff and North-Holland (Elsevier).

[Church, 1936] Alonzo Church. A note on the Entscheidungsproblem. J. Symbolic Logic, 1:40–41,101–102, 1936.

[Cohen & Wartofsky, 1967] Robert S. Cohen and Marx W. Wartofsky, editors. Proc. of the Boston Colloquium for the Philosophy of Science, 1964–1966: In Memory of Norwood Russell Hanson. Number 3 in Boston Studies in the Philosophy of Science. D. Reidel Publ., Dordrecht, now part of Springer Science+Business Media, 1967.

[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, 1971, pp. 1–82].

[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. North-Holland (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, 1969] Gerhard Gentzen. The Collected Papers of Gerhard Gentzen. North-Holland (Elsevier), 1969. Ed. by Manfred E. Szabo.

[Gillman, 1987] Leonard Gillman. Writing Mathematics Well. The Mathematical Association of America, 1987.

[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, 1986ff.] Kurt Gödel. Collected Works. Oxford Univ. Press, 1986ff. Ed. by Sol Feferman, John W. Dawson Jr., Warren Goldfarb, Jean van Heijenoort, Stephen C. Kleene, Charles Parsons, Wilfried Sieg, &al..

[Goldfarb, 1970] Warren Goldfarb. Review of [Herbrand, 1968]. The Philosophical Review, 79:576–578, 1970.

[Heijenoort, 1967] Jean van Heijenoort. Logic as a calculus and logic as a language. Synthese, 17:324–330, 1967. Also in [Cohen & Wartofsky, 1967, pp. 440–446]. Also in [Heijenoort, 1986b, pp. 11–16].

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

[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, The University 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]. Rev. English translation is [Heijenoort, 1986a].

[Heijenoort, 1986a] Jean van Heijenoort. Herbrand’s work in logic and its historical context. 1986. In [Heijenoort, 1986b, pp. 99–121]. Rev. English translation of [Heijenoort, 1982].

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

[Heijenoort, 1992] Jean van Heijenoort. Historical development of modern logic. Modern Logic, 2:242– 255, 1992. Written in 1974.

[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. A contorted, newly typeset reprint is [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, 1971, 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, 1968] Jacques Herbrand. Écrits Logiques. Presses Universitaires de France, Paris, 1968. Cortorted edn. of Herbrand’s logical writings by Jean van Heijenoort. Review in [Goldfarb, 1970]. 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. (This edition is still an excellent source on Herbrand’s writings today, but it is problematic because it is based on the contorted reprint [Herbrand, 1968]. This means that it urgently needs a corrected edition based on the original editions of Herbrand’s logical writings, which are all in French and which should be included in facsimile to avoid future contortion.).

[Hilbert & Bernays, 1934] David Hilbert and Paul Bernays. Die Grundlagen der Mathematik — Erster Band. Number XL in Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen. Springer, 1934. 1^{st} edn. (2^{nd} edn. is [Hilbert & Bernays, 1968]). English translation is [Hilbert & Bernays, 2013a; 2013b].

[Hilbert & Bernays, 1968] David Hilbert and Paul Bernays. Die Grundlagen der Mathematik I. Number 40 in Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen. Springer, 1968. 2^{nd} rev. edn. of [Hilbert & Bernays, 1934]. English translation is [Hilbert & Bernays, 2013a; 2013b].

[Hilbert & Bernays, 2013a] David Hilbert and Paul Bernays. Grundlagen der Mathematik I — Foundations of Mathematics I, Part A: Title Pages, Prefaces, and §§ 1–2. http://wirth.bplaced.net/p/ hilbertbernays, 2013. Thoroughly rev. 2^{nd} edn. (1^{st} edn. College Publications, London, 2011). First English translation and bilingual facsimile edn. of the 2^{nd} German edn. [Hilbert & Bernays, 1968], incl. the annotation and translation of all differences of the 1^{st} German edn. [Hilbert & Bernays, 1934]. Translated and commented by Claus-Peter Wirth. Ed. by Claus-Peter Wirth, Jörg Siekmann, Michael Gabbay, Dov Gabbay. Advisory Board: Wilfried Sieg (chair), Irving H. Anellis, Steve Awodey, Matthias Baaz, Wilfried Buchholz, Bernd Buldt, Reinhard Kahle, Paolo Mancosu, Charles Parsons, Volker Peckhaus, William W. Tait, Christian Tapp, Richard Zach.

[Hilbert & Bernays, 2013b] David Hilbert and Paul Bernays. Grundlagen der Mathematik I — Foundations of Mathematics I, Part B: §§ 3–5 and Deleted Part I of the 1^{st} Edn.. http://wirth.bplaced.net/ p/hilbertbernays, 2013. Thoroughly rev. 2^{nd} edn.. First English translation and bilingual facsimile edn. of the 2^{nd} German edn. [Hilbert & Bernays, 1968], incl. the annotation and translation of all deleted texts of the 1^{st} German edn. [Hilbert & Bernays, 1934]. Translated and commented by Claus-Peter Wirth. Ed. by Claus-Peter Wirth, Jörg Siekmann, Michael Gabbay, Dov Gabbay. Advisory Board: Wilfried Sieg (chair), Irving H. Anellis, Steve Awodey, Matthias Baaz, Wilfried Buchholz, Bernd Buldt, Reinhard Kahle, Paolo Mancosu, Charles Parsons, Volker Peckhaus, William W. Tait, Christian Tapp, Richard Zach.

[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, 1971, pp. 228–251].

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

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

[Turing, 1936/7] Alan M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, Ser. 2, 42:230–265, 1936/7. Received May 28, 1936. Correction in [Turing, 1937].

[Turing, 1937] Alan M. Turing. On computable numbers, with an application to the Entscheidungsproblem. A correction. Proceedings of the London Mathematical Society, Ser. 2, 43:544–546, 1937. Correction of [Turing, 1936/7] according to the errors found by Paul Bernays.

[Whitehead & Russell, 1910–1913] Alfred North Whitehead and Bertrand Russell. Principia Mathematica. Cambridge Univ. Press, 1910–1913. 1^{st} edn..

[Wirth &al., 2009] Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller, and Serge Autexier. Jacques Herbrand: Life, logic, and automated deduction. 2009. In [Gabbay & Woods, 2004ff., Vol. 5: Logic from Russell to Church, pp. 195–254].

[Wirth &al., 2014] Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller, and Serge Autexier. Lectures on Jacques Herbrand as a Logician. SEKI-Report SR–2009–01 (ISSN 1437–4447). SEKI Publications, DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str. 5, D–28359 Bremen, Germany, 2014. Rev. edn. May 2014, ii+82 pp., http://arxiv.org/abs/0902.4682.

[Wirth, 2012] Claus-Peter Wirth. Herbrand’s Fundamental Theorem in the eyes of Jean van Heijenoort. Logica Universalis, 6:485–520, 2012. Received Jan. 12, 2012. Published online June 22, 2012,

http://dx.doi.org/10.1007/s11787-012-0056-7.

[Wirth, 2014] Claus-Peter Wirth. Herbrand’s Fundamental Theorem: The Historical Facts and their Streamlining. SEKI-Report SR–2014–01 (ISSN 1437–4447). SEKI Publications, DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str. 5, D–28359 Bremen, Germany,

2014. ii+45 pp., http://arxiv.org/abs/1405.6317.