I have yet another post about what is model theory doing and why is it valid; I hope I can be coherent.
(1) https://mathoverflow.net/questions/23060/set-theory-and-model-theory
(3) Is an interpretation just a homomorphism between theories?
(4) https://mathoverflow.net/questions/22635/can-we-prove-set-theory-is-consistent
are in a similar vein and since some of them are over 10 year old I decided to make a new post for this discussion, although I want to clarify some of the points people are making there; I will quote the relevant sections.
The Problem
So thankfully it seems Im not alone in finding model theory hard to understand. The confussion for me is "where does it exist"? Is it "meta" or is it internal to ZFC. I think that maybe this is hard because it is a question that actually depends on your foundations / philosophy.
Im adopting a Curry type formalist perspective as a minimal position. My diognosis is that this question is maybe as much about languages as much as models. The question of what a model is will depend on what we think a language is. My position is that a language is the primitive concept that I assume. All else will be built on an intuitive and assumed grasp of what it means to have symbols, move symbols, differentiate symbols etc
A specific instance that im stuggling to understand is how I can interpret in this way the internalization of models of ZFC e.g. in independence proofs.
My understanding
I will outline my attempt at an answer and maybe someone can tell me how to fix it:
We have two languages, these are primitive. One of them is ZFC. A model is a translation of one language into ZFC. It is at the meta-level,it is an act of human computation, specification, at the level of the linguistic primitive of moving symbols around. It needs to satisfy some properties such as "true" in the first language $\implies$ "true" in ZFC.
Here we could take truth to be a primitive associated to languages or define it in terms of the primitives of the language (derivable in a proof system).
I will call this process intuitive modelling for later reference.
If this is what is meant then it is clear that this is not formal (it doesnt exist within a given language, unless we postulate a universal language maybe ...?) it is intuitive at the level of our primitive ideas of language.
Does anyone mean this by model or am I missing the point?
If this is not what they mean then I can only see that they mean something much more mundane, a language is litterally a type of set in ZFC. A model is litterally a function within ZFC.
The only problem with this is then how do we view statements of independence. What is a "model of ZFC + CH"? It cannot be a set in ZFC I beleive for technical reasons (Godel?); but it cannot be a set in ZFC for logio-philosophical reasons, its clearly circular ZFC is a set in ZFC?
Responses
The first response I see is to sort of take mathematics as given and then just say model theory is a part of it and dont worry
A theory is a set of sentences; a model is a "piece of the mathematical world" that satisfies the sentences (axioms) of the theory. ... What are number? What is $\mathbb{N}$ ? It is the set of natural numbers; how we "known" it? How we describe it? With usual mathematical jargon. (2)
or in the first link
if you ask "why are model theorists justified in using sets?" then I ask back "why are number theorists justified in using numbers?" (1)
This is valid but not really helpful for me I guess.
Stefan Hoffelners response in (1) is excellent but im still troubled by these "codings"
As you know, one can code the symbols of first order logic within set theory and, as a consequence, the whole model theory can be carried out in ZFC.
Is this coding not an example of intuitive modelling as I have described above?
Thanks
Im clearly very confused about this, I have tried to be succinct and coherent, questions and clarifications are welcome. Thanks for any engagement.
Model theory (of first order theories) just looks at sets with some relations and functions on them that are appropriate for interpreting formal sentences elaborated on previously specified signatures (some symbols for relations and functions) and according to some (common) grammatical rules (those of first order theories)
Familiar examples include the theory of groups, whose signature includes a binary function symbol (to be interpreted as the product), a unary function symbol (to be interpreted as the inverse function), and a nullary/zero-ary function symbol (to be interpreted as the group identity), and the theory of rings, whose signature you should be able to guess. Now, any set whatsoever 'equipped' with appropriate functions and symbols can in principle be seen as a structure to interpret the sentences formulated in these languages, but only those satisfying - and this is the fundamental concept/notion upon the whole subject is built - some given sentences (the axioms of the theory) are of interest
What about set theory, then? They (there are many) (generally?) are first order theories themselves, so of course they are susceptible to model-theoretic analysis/treatments: their signature consisting of a binary relation symbol, to be interpreted as membership, and their axioms a bunch of sentences elaborated on the usual way of first order theories, a model of a set theory is simply going to be a set with a binary relation
Perhaps we need to take a step back to stress an important point: on the one hand we have symbols, signatures, languages, sentences, axioms, etc., and on the other we have actual objects (sets), with actual functions and relations on them. This may cause some confusion at first: isn't everything on (the usual) set theories just sets? The strict answer is 'yes', so the difference in hands is less of a literal one and more of a 'moral' one: we somehow ought to think of these things as different, for they are qualitatively so, or at least because or intentions towards them are different
Still, what about set theory being used to formulate model theory to begin with? Isn't that somehow "circular"? Well, we do use natural languages to do/study linguistics, and we do cosmology inside the (our?) universe: it's kind of just a fact of life we have to learn to deal with... ok, this sounds sort of dismissive of the problem, so let's think a bit more
Incompleteness issues prevent us from actually proving, from a given set theory, that this set theory has a model, but we can simply assume "Let there be lig... a model", and take it from there: from this moment on, we have a structure, a bona fide object to work with inside our set theory. Notice though that it being a model only ensures it satisfies the axioms insofar as 'satisfy' speaks of its elements behaving in such and such a manner amongst themselves and the specified (functions and) relation(s), it doesn't necessarily mean it somehow relates to the other objects of the ambient/underlying set theory in any 'meaningful way': the most commonly cited example is the powerset, in that an element of the model is going to have a powerset 'inside the model', and this doesn't necessarily have to be equal to the powerset as it exists 'outside'
There are many other intricacies and technicalities regarding model theory of set theories (the huge subject of set theory as commonly now understood basically is model theory of it), but I hope you can find some comfort with the main take away that set theories are first order theories like any other (well, not quite, but anyway), and so it's perfectly legitimate to do model theory of them