I'm learning model theory from Kirby's An Invitation to Model Theory. In a recursive definition of the interpretation of $L$-formulas, he defines $\mathcal A \models (\varphi \wedge \psi)$ to be true iff $\mathcal A \models \varphi$ and $\mathcal A \models \psi$. This makes sense to me, but I wonder whether we could just define $\mathcal A \models (\varphi \wedge \psi)$ to be true iff $\varphi^{\mathcal A} \wedge \psi^{\mathcal A}$, where the second $\wedge$ occurs in the language in which the model $\mathcal A$ is built, and $\varphi^{\mathcal A}$ and $\psi^{\mathcal A}$ denote the inductive interpretations of $\varphi$ and $\psi$ in $\mathcal A$.
For example, suppose $\varphi = R_1(a, b)$ and $\psi = R_2(c)$, where $R_1$ and $R_2$ are relations in $L$ and $a,b$ and $c$ are constants. Then we understand $\varphi^{\mathcal A}$ to denote the statement $(a^{\mathcal A}, b^{\mathcal A}) \in R_1^{\mathcal A}$, and $\psi^{\mathcal A}$ to denote the statement $c^{\mathcal A} \in R_2^{\mathcal A}$. Then it seems to me that $\varphi^{\mathcal A} \wedge \psi^{\mathcal A}$ makes perfect sense as a sentence within ZFC, which is where the model lives. Does it, and is this a valid alternative way to define the interpretation of formulas with connectives like $\wedge$ ?
The main reason I ask is that this brings out a more general confusion I have about what models actually are. The way I currently understand models is as particular sets constructed within first-order ZFC and particular functions and relations on those sets. Since ZFC is a first-order language, it contains sentences with connectives and quantifiers. However, the model theory books I've looked at don't seem to treat models this way—they seem to consider them more like platonic objects that exist without reference to the theory in which they are constructed. So I think answering this question might help clear up some fundamental confusion I have.
Best Answer
Defining satisfaction like this isn't wrong, per se -- in fact there's arguably no real distinction between this and the usual way -- but it puts undue emphasis on the formalization of the metatheory.
This is also not wrong, per se, but it puts undue emphasis on the formalization of the metatheory.
It's better to understand it this way:
Aside from the fact that we often want to use axioms stronger than ZFC (say, to construct models of ZFC), the point is that models are mathematical structures, on the exact same footing as (say) groups or posets. In fact these are just specific instances of models: a group is the exact same thing as a model of the group axioms, and a poset is the exact same thing as a model of the partial order axioms.
And we don't go around saying
because "constructed within first-order ZFC" is either redundant, false, or overly restrictive, depending on your foundational stance and particular aims. (If omitting that clause really did commit us to Platonism, nearly every mathematical exposition in existence would be thoroughly committed to Platonism!)
Perhaps, but it's pretty rare... certainly not worth adding a layer of formalization to our basic definitions just because at some point we might need to delve into philosophy. We can address that if it actually comes up.
But on the other hand, it's true that model theory can be more inherently set-theoretical than most other branches of math (i.e. running into independence phenomena and conjectures that are tied up with large cardinals with some frequency), so it's not outlandish -- probably prudent, in fact -- to be explicit about the fact that we're working in ZFC. But as with any other subject, including set theory itself, we'll mostly be phrasing our arguments and definitions informally, so why should we write a symbol rather than just (equivalently) saying "and"?
(On a side note, I'd venture to say set theorists get a lot more mileage out of explicitly formalizing model theory in set theory than model theorists.)