Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:finite_model_and_infinite_herbrand_model_example [2008/04/01 23:12] vkuncak |
sav08:finite_model_and_infinite_herbrand_model_example [2008/04/01 23:14] 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 18: | Line 18: | ||
Cardinality of Herbrand model is ++|infinite!++ | Cardinality of Herbrand model 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. ++ |