Herbrand's theorem

From Wikipedia, the free encyclopedia

Not to be confused with Herbrand–Ribet theorem.

It has been suggested that Herbrand theory be merged into this article or section. (Discuss)

In mathematical logic, Herbrand's theorem is a basic result of Jacques Herbrand from the 1920s. It essentially states that in formal first-order logic, if a formula in prenex form is satisfiable, then it is satisfiable in a model which interprets logic symbols using terms of the logic itself (i.e. a Herbrand interpretation).

Formally: In predicate logic without equality, a formula $A$ in prenex form (all quantifiers at the front) is provable if and only if a sequent $S$ comprising substitution instances of the quantifier-free subformula of $A$ is propositionally derivable, and $A$ can be obtained from $S$ by structural rules and quantifier rules only.

Let $T$ be a first-order theory consisting of open formulas only. Then:

If $T$ is satisfiable, it has a Herbrand model
If $T$ is not satisfiable, there is a finite subset of the set of ground instances of formulas of $T$ which is unsatisfiable.