LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:preliminary_discussion_on_models [2008/03/20 13:40]
vkuncak
sav08:preliminary_discussion_on_models [2012/04/23 10:17]
vkuncak
Line 1: Line 1:
 ====== Model Sizes ====== ====== Model Sizes ======
  
-We sawif 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 satisfiabilitythe 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 of a model, and this model is countable. 
 +  * this will also give us a systematic method to search for unsatisfiable (and thus, for valid) formulas