A formula is inconsistent iff it is unsatisfiable for any interpretation over any domain. Since there are infinitely many domains and interpretations, it is important not to say what the domain and interpretation are, but to treat them algebraically.

Our algebraic domain is called the * Herbrand universe*; it consists
of all the Skolem constants and all the Skolem functions applied to all
constants, recursively. If there is one constant *a* and one function
*f(x)*, the Herbrand universe will be *{a, f(a), f(f(a)), ...}*.
The set of all predicates applied to members of the Herbrand universe
is called the * Herbrand base*.

Herbrand's Theorem states that if a set of clauses *S* is unsatisfiable,
there is a finite unsatisfiable set *S'* of ground instances of *S*, where
the ground instances are obtained by substituting members of the
Herbrand universe for variables in *S*.