Journal article:

    Samuel R. Buss.
    "On Herbrand's Theorem,"
    In Logic and Computational Complexity,
    Lecture Notes in Computer Science #960, 1995, Springer-Verlag, pp. 195-209.

    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.