Are there true models of $\sf ZFC$

first-order-logicmodel-theoryset-theory

Let $M$ be a transitive model of a $\sf ZFC$, such that for any objects $x_1,..,x_n$ that are elements of the domain of $M$ we have every sentence $\psi(x_1,..,x_n)$ in which all free variables are seen, that is satisfied in $M$, then it is also satisfied about those objects in $\mathcal P^{\text{size}} (M)$. The latter is the set of every subset of $M$ of equal size to an element in $M$. Such model I'd call as a true model of $\sf ZFC$, because all of what it says about objects in it meets what is true about them when viewed externally over element-sized subsets of it. Formally:

$(M, \in) \text{ is a true model of } T \iff (M, \in)\models T \\\land (M \text { is transitive}) \land \forall x_1,..,x_n \in M \forall \psi: \\ (M, \in) \models \psi(x_1,..,x_n) \implies \mathcal (\mathcal P^{\text{size}} (M), \in) \models \psi(x_1,..,x_n)$

Are there true models of $\sf ZFC$?

My guess, is that the true models of $\sf ZFC$, so defined, are the inaccessible ones. But, I'm not sure if there is more into that than just inaccessiblity?

Best Answer

Your guess is correct.

First note that if $κ$ is inaccessible then $\mathcal P^{\text{size}} (V_κ)=V_κ⊨ZFC$ so it is trivially true model.

Now assume $(M,∈)$ is a true model, and $f:\mathcal P^{\text{size}} (M)^n→\mathcal P^{\text{size}} (M)$ is any function (not only definable from $(\mathcal P^{\text{size}} (M), \in)$) and $x\in\mathcal P^{\text{size}} (M)$, then $|f↾x|=|x|$ (from the definition of a function), hence $f↾x\in \mathcal P^{\text{size}} (M)$ which implies $(\mathcal P^{\text{size}} (M),∈)$ is a model of ZFC2, i.e. $(\mathcal P^{\text{size}} (M),∈)≅V_κ$ for some inaccessible $κ$, because $\mathcal P^{\text{size}} (M)$ is transitive we know that this isomorphism is really equality.

Lastly we can now show that if $V_κ=\mathcal P^{\text{size}} (M)$ for inaccessible $κ$ then $\mathcal P^{\text{size}} (M)=M=V_κ$, let $a$ be element in $V_κ\setminus M$, then $\{a\}∈V_κ\setminus M=\mathcal P^{\text{size}} (M)\setminus M$, which implies that $\{a\}⊆M\implies a\in M$, contradiction.

Related Question