# Can we construct a smaller model of ZFC than transitive minimal model?

Let's say there is countable transitive minimal model of ZFC. Then can we construct a smaller nonstandard model of ZFC? How is this possible?

-
I don't see how this question is remotely "elementary set theory". I also removed the model theory tag because this pertains more to classical logic (i.e. completeness/incompleteness) rather than model theoretic methods like ultraproducts, prime models, and so on. –  Asaf Karagila Jun 28 '13 at 0:27

We can prove that such model exists.

Note that transitive models are $\omega$-models, i.e. they agree with the universe on the natural numbers. Since the universe has a model of $\sf ZFC$ it has a proof of the number theoretical statement $\text{Con}(\sf ZFC)$. Therefore if $M$ is any transitive model of $\sf ZFC$, and in particular the minimal one, then $M\models\text{Con}(\sf ZFC)$.

If $L_\alpha$ is the least transitive model then $L_\alpha\models\text{Con}(\sf ZFC)$, so by the completeness theorem $L_\alpha$ knows about a model of $\sf ZFC$, but at the same time this model cannot be transitive (by minimality) so it has to be non-standard.

-
(I couldn't find the link, but I expanded on this a while ago): By $\Sigma^1_1$ absoluteness, any transitive model of set theory (in particular, the minimal transitive model) contains $\omega$-models of set theory, perhaps ill-founded (definitely ill-founded, in the minimal transitive model). By the completeness theorem, any $\omega$-model contains models of set theory (in some cases, only models that are not $\omega$-models). –  Andres Caicedo Jun 28 '13 at 2:55
In fact, we will get a model of $\mathsf{ZFC}+\mathrm{Con}(\mathsf{ZFC}+\mathrm{Con}(\mathsf{ZFC}))$, etc. The moral is that there is a long way to go between the minimal transitive model and any model of $\mathsf{ZFC}+\lnot\mathrm{Con}(\mathsf{ZFC})$, which is the only kind that can genuinely claim to be minimal. But then we can go (a bit) further still: –  Andres Caicedo Jun 28 '13 at 2:58
No such model can be computable (and so, it is not clear how one would formalize the idea that one of these is "minimal"). However, within the arithmetic hierarchy, (good) bounds on the complexity of some such model can be obtained by carefully considering Henkin's proof of the completeness theorem. –  Andres Caicedo Jun 28 '13 at 3:04