A set of universally quantified equality-free first-order clauses is unsatisfiable if and only if some finite set of its ground instances is propositionally unsatisfiable. Equivalently, such a set is satisfiable if and only if it has a Herbrand model. General first-order sentences can first undergo Skolemization. A fresh constant is added if needed to make the Herbrand universe nonempty; first-order equality requires its corresponding equality treatment.
Articles by others on the same topic
Herbrand's theorem is an important result in mathematical logic, particularly in the field of model theory and proof theory. It connects syntactic properties of first-order logic formulas to semantic properties of their models. There are several formulations of Herbrand's theorem, but one of the most common versions concerns the existence of models for a set of first-order logic sentences. ### Herbrand's Theorem (Informal Statement) 1.