Herbrand Universe

Consider a first-order logic formula  in Skolemized form

Then the Herbrand universe  of  is defined by the following rules.

1. All constants from  belong to . If there are no constants in , then  contains an arbitrary constant .

2. If , and an -place function  occurs in , then .

The clauses (disjunctions of literals) obtained from those of  by replacing all variables by elements of the Herbrand universe are called ground clauses, with similar definitions for a ground literal and ground atom. The set of all ground atoms that can be formed from predicate symbols from  and terms from  is called the Herbrand base.

Consecutive generation of elements of the Herbrand universe and verification of unsatisfiability of generated elements can be straightforwardly implemented in a computer program. Given the completeness of first-order logic, this program is basically a tool for automated theorem proving. Of course, this exhaustive search is too slow for practical applications.

This program will terminate on all unsatisfiable formulas and will not terminate on satisfiable formulas, which basically shows that the set of unsatisfiable formulas is recursively enumerable. Since provability (or equivalently unsatisfiability) in first-order logic is recursively undecidable, this set is not recursive.

REFERENCES

Chang, C.-L. and Lee, R. C.-T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997.

Kleene, S. C. Mathematical Logic. New York: Dover, 2002.