Herbrand's Theorem

There are two important theorems known as Herbrand's theorem.

The first arises in ring theory. Let an ideal class be in A if it contains an ideal whose lth power is principal. Let i be an odd integer 1<=i<=l and define j by i+j=1. Then A_1=<e>. If i>=3 and lB_j, then A_i=<e>.

The Herbrand theorem in logic states that a formula Phi is unsatisfiable iff there is a finite set of ground clauses of S that is unsatisfiable in propositional calculus. It is assumed that elements of the Herbrand base are treated as propositional variables. Since unsatisfiability is dual to validity (Phi is unsatisfiable iff the negation !Phi is valid), the Herbrand theorem establishes that the Herbrand universe alone is sufficient for interpretation of first-order logic. This theorem also reduces the question of unsatisfiability in first-order logic to the question of unsatisfiability in propositional calculus.

See also

Ground Clause, Herbrand Universe, Ideal, Unsatisfiable

Portions of this entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha


Ireland, K. and Rosen, M. "Herbrand's Theorem." §15.3 in A Classical Introduction to Modern Number Theory, 2nd ed. New York: Springer-Verlag, pp. 241-248, 1990.

Referenced on Wolfram|Alpha

Herbrand's Theorem

Cite this as:

Sakharov, Alex and Weisstein, Eric W. "Herbrand's Theorem." From MathWorld--A Wolfram Web Resource.

Subject classifications