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. Let be a formula of first-order logic with 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 , possibly in an expansion of the language, with and , such that is valid. If it is valid, it is called a Herbrand disjunction for Informally: a formula 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 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. A proof of the non-trivial direction of the theorem can be constructed according to the following steps: If the formula is valid, then by completeness of cut-free sequent calculus, which follows from Gentzen's cut-elimination theorem, there is a cut-free proof of . Starting from above downwards, remove the inferences that introduce existential quantifiers. Remove contraction-inferences on previously existentially quantified formulas, since the formulas (now with terms substituted for previously quantified variables) might not be identical anymore after the removal of the quantifier inferences.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (2)

Jacques Herbrand

Jacques Herbrand (12 February 1908 – 27 July 1931) was a French mathematician. Although he died at age 23, he was already considered one of "the greatest mathematicians of the younger generation" by his professors Helmut Hasse and Richard Courant. He worked in mathematical logic and class field theory. He introduced recursive functions. Herbrand's theorem refers to either of two completely different theorems. One is a result from his doctoral thesis in proof theory, and the other one half of the Herbrand–Ribet theorem.

Herbrand's theorem