__Journal article:__

** Samuel R. Buss.
"On Herbrand's Theorem,"
**

** Abstract: **We firstly survey several forms of
Herbrand's theorem. What is commonly called ``Herbrand's theorem'' in many textbooks is
actually a very simple form of Herbrand's theorem which applies only to
$\forall\exists$-formulas; but the original statement of Herbrand's theorem applied to
arbitrary first-order formulas. We give a direct proof, based on cut-elimination, of what
is essentially Herbrand's original theorem. The ``nocounterexample theorems'' recently
used in bounded and Peano arithmetic are immediate corollaries of this form of Herbrand's
theorem.

Secondly, we discuss the results proved in Herbrand's 1930
dissertation.

** Download postscript or PDF.**

** Errata.**
The paper contains an error in the proof of Theorem 3, the general form of Herbrand's theorem.
I am grateful to Richard McKinley for discovering this, and for also provided a corrected proof of Theorem 3,
based on "deep contraction". The corrected proof is available in the manuscript "A sequent calculus demonstration of Herbrand's Theorem" by Richard McKinley.

**Back to Sam Buss's publications page.**