What does model-theoretic proofs really prove?

Question

I'm reading David Marker's celebrated textbook, and I have a doubt when applying model theory to classical algebra. I know some basic algebraic facts have model-theoretic proof, such as Hilbert Nullstellensatz. My question is, does this proof and the classical algebraic proof proves the same thing? More precisely, whether it proves $ZFC \vdash \textit{Nullstellensatz}$ or $ZFC \vdash \left( ZFC \vdash \textit{Nullstellensatz} \right)$? Here I suppose the model theory(the theory of $ACF_0$ and its models) was constructed inside a set theory, which is axiomatized by $ZFC$.

Answer 1

Model theory - and logic in general - definitely "ramps up the mystery factor" in mathematical arguments, at least at first. But there's actually nothing special about it; just like (say) the study of partial differential equations, model theory is implicitly developed inside $\mathsf{ZFC}$ and all arguments involving it go through inside $\mathsf{ZFC}$ unproblematically. (OK fine, there are situations where we separately consider stronger axiom systems such as $\mathsf{ZFC}$ + [large cardinals] or $\mathsf{ZFC}$ + [combinatorial principles], but that happens with other fields of math too - just vastly more rarely.)

At its core, model theory is just a continuation of the same line of thought that developed abstract algebra. Abstract algebra has much the same feel of mystery to it at first: somehow we're able to avoid to a large extent direct analyses of the particular structures we care about in favor of broad generalities which somehow manage to solve problems. Galois theory is a great example of this: it's very surprising that general arguments about abstract groups can somehow resolve questions about specific polynomials or compass-and-straightedge problems! "To me, I think they just bypassed the essential difficulty in some logical way" would be a very reasonable response from someone first learning Galois theory, but ultimately there's no trickery going on - and the same is true of model theory, for the same reason.

There are various reasons why model theory is often found to be particularly mysterious. One of these is that by explicitly relating to foundations of mathematics, it draws foundational concerns in a way that abstract algebra doesn't. I think in this case though the primary issue is the subtlety of the classes of structures involved: in place of the classes of groups, rings, fields, and so on we consider general elementary classes, and since first-order logic is much richer than the simple algebraic properties we're used to from abstract algebra this seems much more worrying. But in fact the "informal-but-rigorous" presentation of the semantics of first-order logic translates directly to a formal $\mathsf{ZFC}$ implementation of the same, just as with other situations in mathematics. There is a key aspect of the definition which is new, namely definition by recursion, but this is something which set theory is very good at handling (in fact I'd argue that that's the entire point of set theory, but that's a bit bold).

---

For what it's worth, this is far from the only time that one may reasonably be surprised at the power of set theory. Definitions involving "big quantifications" are also a common point of concern, even outside of logic proper. So this is a type of question that you'll likely revisit over time as you develop a solid understanding of set theory. My general advice, for your particular question and all similar questions, is the following:

• Try to find a specific argument which seems slippery and really dive into it in detail. It's hard to convince yourself that a general type of argument is fine without picking a single instance to focus on.

• Expect set theory to provide tedious but straightforward formalizations of the informal-but-rigorous arguments we make. Don't try to do anything subtle or surprising; instead, look for the tools that will let you do exactly what you want. E.g. model theory begins with Tarski's definition of $\models$, which is a definition by recursion, so it's natural to look to the recursion theorem for help there.