Non-Compactness and Incompleteness

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.

Non-Compactness Theorem: Herbrand Logic is not compact.

Proof. Consider the following infinite set of sentences.

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.

Corollary (Infinite Proofs): In Herbrand Logic, some entailed sentences have only infinite proofs.

Proof. The above proof demonstrates a set of sentences that entail ∀x.p(x). The set of premises in any finite proof will be missing one of the above sentences; thus, those premises do not entail ∀x.p(x). Thus no finite proof can exist for ∀x.p(x).

The statement in this Corollary was made earlier with the condition that checking whether a candidate proof actually proves a conjecture is decidable. There is no such condition on this theorem.