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
As Andrés points out in the comments, your question seems to be resolved by the observation that not every model of PA can arise as the $\mathbb{N}$ of a model of ZFC.
Meanwhile, one can attempt to understand more deeply exactly which models of PA do arise as the $\mathbb{N}$ of a model of set theory. Let us say that a model $N\models\text{PA}$ is a standard model of arithmetic (as opposed to the standard model of arithmetic), or alternatively is a ZFC-standard model of arithmetic, if $N=\mathbb{N}^M$ for some $M\models\text{ZFC}$.
Thus, a model of arithmetic is a standard model of arithmetic, if it is the standard model of arithmetic from the perspective of some model of set theory. These are the models of PA that seem to be at the heart of your question.
We can characterize exactly what these models are as follows.
Theorem. (Ali Enayat) The following are equivalent, for a countable nonstandard model $N\models\text{PA}$.
$N$ arises as $\mathbb{N}^M$ for some model $M\models\text{ZFC}$.
$N$ is computably saturated and satisfies all the arithmetic consequences of ZFC.
In statement 2, what we mean is that $N\models\varphi$, whenever $\varphi$ is an arithmetic statement that is provable from ZFC. For example, this includes the case where $\varphi$ is Goodstein's theorem, and this is exactly what is going on in your question. Obviously, any model of PA arising as the $\mathbb{N}$ of a model of ZFC set theory must satisfy all the arithmetic consequences of ZFC, and this is essentially how you are reasoning in statement 3 of the question. The interesting part is that this is also sufficient, when combined with computable saturation.
You can find a proof of the theorem in my paper: J. D. Hamkins and R. Yang, Satisfaction is not absolute, to appear in the Review of Symbolic Logic, pp. 1-34. (arxiv:1312.0670) (see proposition 3).