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

Then

is valid if and only if there exists a finite sequence of terms ${\displaystyle t_{ij}}$, possibly in an expansion of the language, with

such that

is valid. If it is valid,

is called a Herbrand disjunction for

Informally: a formula ${\displaystyle A}$ in prenex form containing existential quantifiers only is provable (valid) in first-order logic if and only if a disjunction composed of substitution instances of the quantifier-free subformula of ${\displaystyle A}$ is a tautology (propositionally derivable).

...
Wikipedia