Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:finite_model_and_infinite_herbrand_model_example [2008/04/01 23:12] vkuncak |
sav08:finite_model_and_infinite_herbrand_model_example [2009/05/14 12:41] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Formulas with Finite Model but Infinite Herbrand Model ====== | + | ====== Formulas with only Finite Models but Infinite Set of Ground Terms ====== |
Example: | Example: | ||
Line 10: | Line 10: | ||
What are possible cardinalities for models? ++| they all have exactly two elements.++ | What are possible cardinalities for models? ++| they all have exactly two elements.++ | ||
- | What is Herbrand model for this formula? ++++| | + | What are ground terms for this formula? ++++| |
\[ | \[ | ||
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 \} | ||
Line 16: | Line 16: | ||
++++ | ++++ | ||
- | 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. ++ | + | 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. ++ |