Herbrand's theorem
Herbrand's theorem is a fundamental result of mathematical logic obtained by Jacques Herbrand (1930). It essentially allows a certain kind of reduction of first-order logic to propositional logic. Although Herbrand originally proved his theorem for arbitrary formulas of first-order logic, the simpler version shown here, restricted to formulas in prenex form containing only existential quantifiers, became more popular. Statement. Let be a formula of first-order logic with formula_2 quantifier-free, though it may contain additional free variables. This version of Herbrand's theorem states that the above formula is valid if and only  if there exists a finite sequence of terms formula_3, possibly in an expansion of the language, with such that is valid. If it is valid, it is called a "Herbrand disjunction" for Informally: a formula formula_8 in prenex form containing only existential quantifiers is provable (valid) in first-order logic if and only if a disjunction composed of substitution instances of the quantifier-free subformula of formula_8 is a tautology (propositionally derivable). The restriction to formulas in prenex form containing only existential quantifiers does not limit the generality of the theorem, because formulas can be converted to prenex form and  their universal quantifiers can be removed by Herbrandization. Conversion to prenex form can be avoided, if "structural" Herbrandization is performed. Herbrandization can be avoided by imposing additional restrictions on the variable dependencies allowed in the Herbrand disjunction. Proof sketch. A proof of the non-trivial direction of the theorem can be constructed according to the following steps: However, sequent calculus and cut-elimination were not known at the time of Herbrand's theorem, and Herbrand had to prove his theorem in a more complicated way.