Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:finite_model_and_infinite_herbrand_model_example [2008/04/01 23:11] vkuncak created |
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 16: | Line 16: | ||
| ++++ | ++++ | ||
| - | By Herbrand theorem, does every satisfiable first-order logic formula have Herbrand model? ++| Only if formula has no equality. ++ | + | 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! We made this assumption when proving Herbrand theorem. ++ | ||