  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\'eor\`eme 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\"owenheim'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\'eorie de la d\'emonstration --- submitted by Jacques Herbrand
(1908-1931) in 1929 at the University of Paris. Herbrand's Fundamental Theorem
is, together with G\"odel'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.
