Show that a set has no Herbrand model

Question

Given the Herbrand Theorem

A clausal theory Th is satisfiable iff the grounding of Th is satisfiable

And given $S = \{ G(c), B(a), G(x) \vee \neg G(y), \neg B(x) \vee \neg G(x) \}$

How can I show that set $S$ has no Herbrand model?

I'm new to logic and have never had any experience in proofs before, what are the steps I should take to approach this? I've looked at Intuition about Herbrand Models. but I'm not quite clear on the Lemma, could someone elaborate a little more? (Sorry for the newbie question!)

Answer 1

As per the linked post, the Herbrand structure is a mathematical structure built with the syntactical stuff: terms are used as objects of the domain of the interpretation.

We consider the set $S$ of clauses. In it we have only two constants : $a$ and $c$. Thre are no function symbols; thus, the only two ground terms are $a$ and $c$.

This means that the H-universe will be: $H = \{ a, c \}$.

Having the domain $H$, we build the interpretation: constants are interpreted with themselves, and predicates are interpreted through ground instances obtained from clauses replacing variables with ground terms.

With $H$ we may generate the following set $S'$ of ground instances :

$\{ G(c), B(a), G(a) \lor ¬ G(c), ¬ B(a) \lor ¬ G(a) \}$.

$S'$ s a finite set of ground instances of the set $S$ of clauses and it is clearly unsatisfiable.

Thus, by Herbrand's Theorem, also the set $S$ is unsatisfiable.

---

We may use Resolution to prove that $S$ is unsatisfiable :

1) $G(c)$

2) $B(a)$

Unifying $¬ B(x) \lor ¬ G(x)$ with $a \to x$ we get $¬ B(a) \lor ¬ G(a)$ and using 2) we get, by Resolution:

3) $¬ G(a)$

Unifying $G(x) \lor ¬ G(y)$ with $a \to x$ and $c \to y$ we get $G(a) \lor ¬ G(c)$ and using 3) we get, by Resolution:

4) $¬ G(c)$

Finally, using Resolution with 1) and 4) we get :

5) $\square$ --- the empty clause, showing the unsatisfiability of $S$.

which is cleary unsatisfiable.