> Hmm. So which n is special in the model that you get from the model existence theorem? Doesn't it all get somehow equivalence-classed away? The model existen

> Hmm. So which n is special in the model that you get from the model existence theorem? Doesn't it all get somehow equivalence-classed away? The model existence theorem relies on extending your original language (and therefore your theory) with a bunch of new constants. So in this case you would end up conjuring up a specific new constant symbol just for `Special`. You then "forget" about all those constants when you retract back to your original theory and so you lose the one-to-one relationship. So it is true that if your original theory is Henkin (i.e. there is a constant symbol witnessing every single existential statement you have) and maximally consistent, then there exists a model that coincides exactly with your theory, in particular the model that is constructed from all your constant symbols modulo equality in your theory. But most theories are not Henkin. And moreover most theories are not maximally consistent (since that would imply completeness in the sense of Godel's incompleteness theorems). In particular the theory you get out of the model existence theorem is usually not computably enumerable, so you can't actually write down your extended theory. So most theories do not have that nice property that they correspond exactly with the semantic properties of a model.