This is an old revision of the document!
Formulas with only Finite Models but Infinite Set of Ground Terms
Example: \[
P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b)
\]
What are possible cardinalities for models?
What are ground terms for this formula?
Cardinality of Herbrand model is
By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model?