Herbrand’s theorem

According to Herbrand’s theorem, each formula F of quantification theory can be associated with a sequence F₁, F₂, F₃,… of quantifier-free formulas such that F is provable just in case F_n is truth-functionally valid for some n. This theorem was the centrepiece of Herbrand’s dissertation, written in 1929 as a contribution to Hilbert’s programme. It provides a finitistically meaningful interpretation of quantification over an infinite domain. Furthermore, it can be applied to yield various consistency and decidability results for formal systems. Herbrand was the first to exploit it in this way, and his work has influenced subsequent research in these areas. While Herbrand’s approach to proof theory has perhaps been overshadowed by the tradition which derives from Gentzen, recent work on automated reasoning continues to draw on his ideas.