Herbrand's theorem

Not to be confused with Herbrand–Ribet theorem or Herbrand's theorem on ramification groups.

Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930).[1] It essentially allows a certain kind of reduction of first-order logic to propositional logic. Herbrand's theorem is the logical foundation for most automatic theorem provers. Although Herbrand originally proved his theorem for arbitrary formulas of first-order logic,[2] the simpler version shown here, restricted to formulas in prenex form containing only existential quantifiers, became more popular.

  1. ^ J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.
  2. ^ Samuel R. Buss: "Handbook of Proof Theory". Chapter 1, "An Introduction to Proof Theory". Elsevier, 1998.