Herband model for a forumla

Question

I need to find a Herband model for the formula $Pc \land \forall x (\exists y (Px \leftrightarrow \neg Py))$, where $c$ is a constant and $P$ is a unary relation. I've already read the theory but unfortunately don't understand how to proceed in practice. It would be nice if someone can help me with some hints.

Thanks in advance.

Answer 1

Ref. to Resolution.

1) Transform the formula in a set $s$ of clauses in Conjunctive Normal Form, removing the universal quantifiers and replacing existentially-quantified variables by Skolem functions:

$S = \{ Pc, ¬Px \lor ¬Pf(x), Pf(x) \lor Px \}$.

2) Build the Herbrand universe with constant and function symbols.

Having only the constant $c$ and the skolem function $f$, the H-universe will be:

$U = \{ c, f(c), f(f(c)), \ldots \}$.

3) Build the Herbrand base for the set $S$ of clauses, i.e. the set of all ground atoms of the form $P(t)$ for the only predicate symbol occurring in $S$ using the closed terms in $U$:

$H_b = \{ Pc, Pf(c), Pf(f(c)), \ldots \}$.

Finally:

4) build the Herbrand interpretation:

every constant is interpreted as itself, and every function symbol is interpreted as the function that applies it. The interpretation also defines predicate symbols as denoting a subset of the relevant Herbrand base, effectively specifying which ground atoms are true in the interpretation. This allows the symbols in a set of clauses to be interpreted in a purely syntactic way, separated from any real instantiation.

In your example:

$H_I= \{ Pc, ¬Pc \lor \lnot Pf(c), Pf(c) \lor Pc, \ldots \}$.

---

See:

• Chin-Liang Chang & Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving (1973), Ch.4 : Herbrand's Theorem, page 45-on.

---

---

You can compare it with a "minimal" model $\mathcal M$ with universe $\{ a , b \}$ such that:

$c^{\mathcal M} = a$ and $P^{\mathcal M} = \{ a \}$.