J. D. Hamkins and C. Leahy, Algebraicity and implicit definability in set theory (also at the arxiv), under review.
We aim in this article to analyze the effect of replacing several natural uses of definability in set theory by the weaker model-theoretic notion of algebraicity and its companion concept of implicit definability. In place of the class HOD of hereditarily ordinal definable sets, for example, we consider the class HOA of hereditarily ordinal-algebraic sets. In place of the pointwise definable models of set theory, we examine its (pointwise) algebraic models. And in place of Gödel's constructible universe L, obtained by iterating the definable power set operation, we introduce the implicitly constructible universe Imp, obtained by iterating the algebraic or implicitly definable power set operation. In each case we investigate how the change from definability to algebraicity affects the nature of the resulting concept. We are especially intrigued by Imp, for it is a new canonical inner model of ZF whose subtler properties are just now coming to light. Open questions about Imp abound.
Before proceeding further, let us review the basic definability definitions. In the model theory of first-order logic, an element $a$ is definable in a structure $M$ if it is the unique object in $M$ satisfying some first-order property $\varphi$ there, that is, if $M\models\varphi[b]$ just in case $b=a$. More generally, an element $a$ is algebraic in $M$ if it has a property $\varphi$ exhibited by only finitely many objects in $M$, so that $\{b\in M \mid M\models\varphi[b]\}$ is a finite set containing $a$. For each class $P\subset M$ we can similarly define what it means for an element to be $P$-definable or $P$-algebraic by allowing the formula $\varphi$ to have parameters from $P$.
In the second-order context, a subset or class $A\subset M^n$ is said to be definable in $M$, if $A=\{\vec a\in M\mid M\models\varphi[\vec a]\}$ for some first-order formula $\varphi$. In particular, $A$ is the unique class in $M^n$ with $\langle M,A\rangle\models\forall \vec x\, [\varphi(\vec x)\iff A(\vec x)]$, in the language where we have added a predicate symbol for $A$. Generalizing this condition, we say that a class $A\subset M^n$ is implicitly definable in $M$ if there is a first-order formula $\psi(A)$ in the expanded language, not necessarily of the form $\forall \vec x\, [\varphi(\vec x)\iff A(\vec x)]$, such that $A$ is unique such that $\langle M,A\rangle\models\psi(A)$. Thus, every (explicitly) definable class is also implicitly definable, but the converse can fail. Even more generally, we say that a class $A\subset M^n$ is algebraic in $M$ if there is a first-order formula $\psi(A)$ in the expanded language such that $\langle M,A\rangle\models\psi(A)$ and there are only finitely many $B\subset M^n$ for which $\langle M,B\rangle\models\psi(B)$. Allowing parameters from a fixed class $P\subset M$ to appear in $\psi$ yields the notions of $P$-definability, implicit $P$-definability, and $P$-algebraicity in $M$. Simplifying the terminology, we say that $A$ is definable, implicitly definable, or algebraic over (rather than in) $M$ if it is $M$-definable, implicitly $M$-definable, or $M$-algebraic in $M$, respectively. A natural generalization of these concepts arises by allowing second-order quantifiers to appear in $\psi$. Thus we may speak of a class $A$ as second-order definable, implicitly second-order definable, or second-order algebraic. Further generalizations are of course possible by allowing $\psi$ to use resources from other strong logics.
The main theorems of the paper are:
Theorem. The class of hereditarily ordinal algebraic sets is the same as the class of hereditarily ordinal definable sets: $$\text{HOA}=\text{HOD}.$$
Theorem. Every pointwise algebraic model of ZF is a pointwise definable model of ZFC+V=HOD.
In the latter part of the paper, we introduce what we view as the natural algebraic analogue of the constructible universe, namely, the implicitly constructible universe, denoted Imp, and built as follows:
$$\text{Imp}_0 = \emptyset$$
$$\text{Imp}_{\alpha + 1} = P_{imp}(\text{Imp}_\alpha)$$
$$\text{Imp}_\lambda = \bigcup_{\alpha < \lambda} \text{Imp}_\alpha, \text{ for limit }\lambda$$
$$\text{Imp} = \bigcup_\alpha \text{Imp}_\alpha.$$
Theorem. Imp is an inner model of ZF with $L\subset\text{Imp}\subset\text{HOD}$.
Theorem. It is relatively consistent with ZFC that $\text{Imp}\neq L$.
Theorem. In any set-forcing extension $L[G]$ of $L$, there is a further extension $L[G][H]$ with $\text{gImp}^{L[G][H]}=\text{Imp}^{L[G][H]}=L$.
Open questions about Imp abound. Can $\text{Imp}^{\text{Imp}}$ differ from $\text{Imp}$? Does $\text{Imp}$ satisfy the axiom of choice? Can $\text{Imp}$ have measurable cardinals? Must $0^\sharp$ be in $\text{Imp}$ when it exists? (An affirmative answer arose in conversation with Menachem Magidor and Gunter Fuchs, and we hope that $\text{Imp}$ will subsume further large cardinal features. We anticipate a future article on the implicitly constructible universe.) Which large cardinals are absolute to $\text{Imp}$? Does $\text{Imp}$ have fine structure? Should we hope for any condensation-like principle? Can CH or GCH fail in $\text{Imp}$? Can reals be added at uncountable construction stages of $\text{Imp}$? Can we separate $\text{Imp}$ from HOD? How much can we control $\text{Imp}$ by forcing? Can we put arbitrary sets into the $\text{Imp}$ of a suitable forcing extension? What can be said about the universe $\text{Imp}(\mathbb{R})$ of sets implicitly constructible relative to $\mathbb{R}$ and, more generally, about $\text{Imp}(X)$ for other sets $X$? Here we hope at least to have aroused interest in these questions.
Best Answer
I highly recommend reading Andrej Bauer's excellent answer to an earlier question along the same lines. To summarize the situation in a few words: the fact that set theory is anterior to model theory does not preclude the model theoretic study of set theoretic structures. The reason for that is the same as why we can study the ring Z even though integers are conceptually anterior to abstract algebra.
I will attempt to answer your revised question as I understand it.
First, it is important to note that set theorists only rarely work with general models of ZFC, so it would be unfair to reduce set theory to the model theory of ZFC. Indeed, set theorists almost exclusively work with well-founded models of (fragments of) ZFC. In fact, the models that set theorists consider are usually of the form (M,∈) where M is a set and ∈ is the true membership relation. While model theoretic ideas play a very important role in set theory, this is very different from how a model theorist would approach models of a given theory.
Second, the language commonly used by set theorists is designed to accomodate multiple philosophical views and focus on the mathematical ideas. When dealing with forcing, set theorist often use a lingo popularized by Baumgartner. In this lingo, one talks of the generic extension V[G] as an object of the same level and equally tangible as the set theoretic universe V. This is easily translated in the multiverse view, but it is just as easy to think of this as no more than a linguistic convenience: set theorists who prefer working with countable transitive models à la Kunen can mentally replace V by such a model M and interpret the words as those of an inhabitant of M; set theorists who prefer working with boolean valued models à la Jech can simply interpret the generic filter G as a convenient abstraction; set theorists who prefer the formal approach can translate the lingo into purely syntactic arguments; etc. In my case, none of these translations ever take place, but I do hold the possibilities in a safe place for comfort.
In conclusion, my advice is to focus on the mathematics and use models as tools just like any other mathematical object.