In light of the negative results described in the last section, namely that Herbrand Logic is inherently incomplete, it is not surprising that Herbrand Logic is not compact. Recall that Compactness says that if an infinite set of sentences is unsatisfiable, there is some finite subset that is unsatisfiable. It guarantees finite proofs.
NonCompactness Theorem: Herbrand Logic is not compact.
Proof. Consider the following infinite set of sentences.
p(a), p(f(a)), p(f(f(a))), ...
Assume the vocabulary is {p, a, f}. Hence, the ground terms are a, f(a), f(f(a)), .... This set of sentences entails ∀x.p(x). Add in the sentence ∃x.¬p(x). Clearly, this infinite set is unsatisfiable. However, every finite subset is satisfiable. (Every finite subset is missing either ∃x.¬p(x) or one of the sentences above. If it is the former, the set is satisfiable; and, if it is the latter, the set can be satisfied by making the missing sentence false.) Thus, compactness does not hold.
