After reading Kunen's section on Model Theory in his Set Theory (2011), I'm still unsure about how model theory is formally developed within ZFC.
I was under the impression that all the symbols required to do model theory would be inherited from the metatheory. For instance, I thought:
1) the symbols used for variables, logical connectives, etc in model theory were the same as those used in the metatheory
2) symbols such as "$\models$" and "$\preccurlyeq$" were gotten from extensions by definitions of the metatheory.
But, I realized 1) is incorrect, since in model theory a signature $L$ can have more symbols than there are in the metatheory. (ie arbitrary cardinality).
So my main issue here is that I can't see where these symbols are coming from.
Does anyone know of any other source that can help clear this up for me? Any help is appreciated. Thanks
Everything can be developed within a model of $\mathsf{ZF}$. Recall that a language is a tuple $\langle \mathsf{Rel},\mathsf{Func},\mathsf{Const},\sigma\rangle$ where $\sigma$ is the arity function. It takes a symbol and returns its arity which is a natural number.
The other elements in the tuple are sets, which may or may not be empty, but we require them all to be disjoint. Take any set which is large enough to hold all the symbols and simply use its elements as the symbols for $\mathsf{Rel,Func}$ and $\mathsf{Const}$. We can assume without loss of generality that we also included in our set fixed symbols for quantifiers, connectives and variables.
Next we want to define terms and [well-formed-]formulas. Those are just finite strings over our language, and if we're not fussy at all, then we can even allow ourselves to have finite strings of finite strings and so save ourselves the trouble of encoding everything into Polish notation.
Recall that we have very strict rules about how to create terms and formulas, and those rules ensure that given a formula the relation of being a "sub-formula" or "sub-term" is a well-founded relation. This ensures that we can easily identify when a finite sequence is syntactically valid.
Next we define the structure. This, again, is a very usual definition, we interpret the language over some non-empty set. And we define an assignment from the variables to the universe of the structure simply as a function, from which we can calculate - again by recursion - whether or not a formula $\varphi$ is true or not when using $s$ to assign values to variables.
This allows us to define the $\models$ relation between a structure and a sentence; and it allows us to define $\implies$ (logical implication); and it allows us to define elementary submodel, or elementary equivalence; and so on.
Note that we really just build things from the bottom up. We start with sets, then we use them to encode the language, then the well-formed formulas, then structures, the satisfaction relation between a structure and a formula, then we can talk about models of a theory, and elementary equivalence, and so on.
If we couldn't do that within $\mathsf{ZF}$ then it wouldn't be a good foundational theory. But it is, and we can.