There are two important theorems known as Herbrand's theorem.
The first arises in ring theory. Let an ideal class be in 
if it contains an ideal whose 
th power is principal. Let
be an odd integer 
and define 
by 
. Then 
. If 
and 
, then 
.
The Herbrand theorem in logic states that a formula 
is unsatisfiable iff
there is a finite set of ground clauses of 
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 (
is unsatisfiable iff
the negation 
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.
