This is an old revision of the document!
Example:
\[
P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b)
\]
Is this formula satisfiable? yes
What are possible cardinalities for models? they all have exactly two elements.
What is Herbrand model for this formula?
\[
GT = \{ a, b, f(a), f(b), f(f(a)), f(f(b)), \ldots \}
\]
By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model? Only if formula has no equality.