> Take the theory of the natural numbers with the new symbol "Special" and the axiom "there exists a number n such that Special(n) holds." In every model of that theory there will be a concrete n that is Special (say 6). However, the theory will never be able to prove that a specific n is Special, precisely because it is under-specified which n it is.
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?
> No in conjunction with Godel's completeness theorem, the incompleteness theorem would say rather that there is no theory that is strictly only the "full" version of arithmetic. Any theory will always be too broad and have too many models that satisfy it, only one of which is the "usual" model of arithmetic.
Sure. The point is that there's always a gap between the theory and the model, an "implementation-defined" part of the model.
> 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.
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?
> No in conjunction with Godel's completeness theorem, the incompleteness theorem would say rather that there is no theory that is strictly only the "full" version of arithmetic. Any theory will always be too broad and have too many models that satisfy it, only one of which is the "usual" model of arithmetic.
Sure. The point is that there's always a gap between the theory and the model, an "implementation-defined" part of the model.