# Differences

This shows you the differences between two versions of the page.

 sav08:finite_model_and_infinite_herbrand_model_example [2009/05/14 12:40]vkuncak sav08:finite_model_and_infinite_herbrand_model_example [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2009/05/14 12:41 vkuncak 2009/05/14 12:40 vkuncak 2008/04/01 23:14 vkuncak 2008/04/01 23:12 vkuncak 2008/04/01 23:11 vkuncak created Next revision Previous revision 2009/05/14 12:41 vkuncak 2009/05/14 12:40 vkuncak 2008/04/01 23:14 vkuncak 2008/04/01 23:12 vkuncak 2008/04/01 23:11 vkuncak created Line 2: Line 2: Example: Example: - $+ \begin{equation*} P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b) 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?​ ++| yes++ Is this formula satisfiable?​ ++| yes++ Line 11: Line 11: What are ground terms for this formula? ++++| What are ground terms for this formula? ++++| - $+ \begin{equation*} GT = \{ a, b, f(a), f(b), f(f(a)), f(f(b)), \ldots \} GT = \{ a, b, f(a), f(b), f(f(a)), f(f(b)), \ldots \} -$ + \end{equation*} ++++ ++++ - Cardinality ​of Herbrand model is ++|infinite!++ + Cardinality is ++|infinite!++ By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model? ++| Only if formula has no equality! ​ We made this assumption when proving Herbrand theorem. ++ By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model? ++| Only if formula has no equality! ​ We made this assumption when proving Herbrand theorem. ++