Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
sav08:preliminary_discussion_on_models [2008/03/20 13:40] vkuncak |
sav08:preliminary_discussion_on_models [2009/05/14 12:34] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Model Sizes ====== | ====== Model Sizes ====== | ||
| - | We saw: if formula has a model of some size, it has many models of same size, from [[Isomorphism of Interpretations]]. | + | Difficulty in semantic definition of validity and satisfiability: the definitions talk about **arbitrary** models (finite models, integers, real numbers, set theory, ...) |
| + | |||
| + | If formula has a model of some size, it has many models of same size, from [[Isomorphism of Interpretations]]. | ||
| Are there first-order formulas that have only finite models? | Are there first-order formulas that have only finite models? | ||
| Line 7: | Line 9: | ||
| Are there first-order formulas that have only infinite models? | Are there first-order formulas that have only infinite models? | ||
| - | What is the cardinality of the models we need to consider? There are many useful models whose domain is not a [[countable set]]. | + | What is the cardinality of the models we need to consider? There are many useful models whose domain is not a [[countable set]] (e.g. real numbers). |
| Difficulty in checking $\models S$: there are infinitely many models, of arbitrarily large cardinalities. | Difficulty in checking $\models S$: there are infinitely many models, of arbitrarily large cardinalities. | ||
| Goal: show that if a set $S$ of formulas has a model, then it has a particular kind, and this model is countable. | Goal: show that if a set $S$ of formulas has a model, then it has a particular kind, and this model is countable. | ||
| + | * this will also give us a systematic method to search for unsatisfiable (and thus, for valid) formulas | ||
| + | |||