LARA

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)

\]

Is this formula satisfiable?

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?