On Herbrand's theorem

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 ℬ∃-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.