LARA

Formulas with only Finite Models but Infinite Set of Ground Terms

Example:

\begin{equation*}
    P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b)
\end{equation*}

Is this formula satisfiable?

What are possible cardinalities for models?

What are ground terms for this formula?

Cardinality is

By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model?