Herbrand theorem works only with clauses

Question

I read that Herbrand's theorem is valid only for a set of clauses. I already know how to convert every formula in a clause. But, what I haven't understood is why Herbrand's theorem doesn't work with a formula that's not a clause. Can you show me ?

Answer 1

See: Mordechai Ben-Ari, Mathematical Logic for Computer Science, Springer (3rd ed 2012), page 180:

Herbrand’s Theorem: A set of clauses $S$ is unsatisfiable if and only if a finite set of ground instances of clauses of $S$ is unsatisfiable.

From this we have that: a set of clauses $S$ is unsatisfiable iff $S$ has no Herbrand models.

The restriction that $S$ be a set of clauses is unavoidable, i.e. if $S$ is a set of arbitrary closed formulas, it is not possible, in general, to show that $S$ is unsatisfiable considering only to Herbrand interpretations.

Let $S = \{ \ p(a), \ \exists x \lnot p(x) \ \}$, where the second formula is not a clause.

Obviously, $S$ has a model: let $D = \{ 0, 1 \}$ and assign $0$ to $a$. Then, interpret $p$ with the function which maps $0$ to TRUE and $1$ to FALSE.

The only Herbrand interpretations for $S$ are $\emptyset$ and $\{ p(a) \}$ (there are no function symbols in $S$), but neither of these is a model for $S$.

Conclusion: $S$ does not have an Herbrand model.