I’ve been reading the basics on model theory from Kunen’s Set Theory, and have a few questions of the foundational kind. If at any point I do not make myself clear, I’ll try to elaborate to the best of my capacity,
One can construct model theory within ZFC: given a set of symbols $\mathcal{L}$ (partitioned into functions and relations by arity), we can recursively construct the set of well formed formulas as a certain subset of $(\mathcal{W}\cup \mathcal{L})^{<\omega}$, where $\mathcal{W}$ is the set of logical symbols (connectives, $=$, quantifiers, etc), which can be taken to be some subset of the natural numbers (the actual choice is irrelevant). Then, one defines a $\mathcal{L}$-structure as a pair $\mathfrak{A}=(A,\mathcal{I})$, where $\mathcal{I}$ is a map which assigns to each symbol in $\mathcal{L}$ a semantic entity in $A$ of the corresponding type (for instance, if $f\mathcal{L}$ is an $n$-ary function symbol, then $\mathcal{I}(f)=f^\mathfrak{A}:A^n\to A$). We can then use this framework to study different first order theories, such as rings, groups, etc. I start to have doubts when one tries to apply this to study models of set theory itself, which gives us a coding of the formulas of set theory (written in $\{\in\}$), which are objects of the meta theory, within ZFC, as actual sets. However, what is the set of symbols for this coding? Intuitively, its $\{\in\}$, but $\in$ is not an object of ZFC (not a set), but rather a logical symbol. So, what’s going on? I guess we could just define $\in$ to be some arbitrary set $t$ and then consider the formulas written in the language $\{t\}$ and then adequately interpreting everything, but can’t this approach run into some issues regarding unique readability?
On a related note, I see no problem with the actual models of set theory, one can just define a $\in$-model as a pair $(A,E_A)$ with $E_A:=\{(a,b)\in A\times A:a\in b\}$, but to write $(A,E_A)\models \phi$ for a coded formula of set theory $\phi$, one needs to know the language the coding is written in.