Is the minimal transitive model of $\sf ZFC$ pointwise definable?


If not, then what is the minimal pointwise definable model of $\sf ZFC$?


Can we define that using [Hamkins](http://jdh.hamkins.org/pointwisedefinablemodelsofsettheory/) result for existence of class forcing extensions of every countable model of $\sf ZFC$ that are pointwise definable? Would it be the extension of the minimal transitive model of $\sf ZFC$ using Hamkins result?



Which model is the minimal pointwise definable model of $\sf ZFC$?
Yes, the minimal transitive model of ZFC is pointwise definable.


The minimal transitive model of ZFC, known as the [Shephardson-Cohen model](https://en.wikipedia.org/wiki/Minimal_model_(set_theory)), is the model $\langle L\_\alpha,\in\rangle$, where the ordinal $\alpha$ is smallest such that this is a model of ZFC.


Let me make a few observations about it.


* The minimal model is not only minimal, but least. That is, if $M$ is any transitive model of ZFC, then the constructible universe $L^M$ of that model will also be a model of ZFC and have the form $L\_\gamma$, and so the minimal model $L\_\alpha$ will be contained within it.
* It follows that the minimal transitive model of ZFC exists if and only if there is a transitive model of ZFC.
* The minimal model might not exist — it is consistent with ZFC that there is no transitive model of ZFC. For example, in the minimal model $L\_\alpha$ itself, there is no element that is a transitive model of ZFC. So it is consistent with ZFC that the minimal model does not exist.
* The existence of the minimal transitive model of ZFC has some mild consistency strength. If there is a transitive model $M$ of ZFC, then of course Con(ZFC) must hold. But since the model is transitive, we get Con(ZFC) holding inside $M$, and so Con(ZFC+Con(ZFC)) holds. But then this holds also inside $M$, and so Con(ZFC+Con(ZFC+Con(ZFC))) holds, and so on. One can iterate this process transfinitely. So the existence of the minimal model implies a tower of iterated consistency statements transcending ZFC.


**Theorem.** The minimal transitive model of ZFC is pointwise definable.


**Proof.** Suppose that $L\_\alpha$ is the minimal transitive model of ZFC. This model satisfies $V=L$ and consequently has a definable global well ordering of the universe. This implies that the model has definable Skolem functions, picking out the least witness for any existential property. The set of definable elements of $L\_\alpha$ is therefore closed under Skolem witnesses and is therefore an elementary substructure of $L\_\alpha$. By condensation, this collection is isomorphic by the Mostowski collapse to a model $L\_\beta$, which must be a model of ZFC, and which furthermore is pointwise definable, since we had included only definable elements. Since $\beta\leq\alpha$, it follows by minimality that $\beta=\alpha$. And so $L\_\alpha$ is pointwise definable. $\Box$


If one equips the minimal transitive model of ZFC with all its definable classes, then one achieves a minimal transitive model of Gödel-Bernays GBC set theory.


Meanwhile, Kameryn Williams proved in his dissertation result that there is no minimal transitive model of Kelley-Morse set theory.


* *Williams, Kameryn J.*, [**Minimum models of second-order set theories**](https://doi.org/10.1017/jsl.2019.27), J. Symb. Log. 84, No. 2, 589-620 (2019). [ZBL1453.03033](https://zbmath.org/?q=an:1453.03033).


The forcing paper you mention is the following, where we proved that every countable model of ZFC and indeed GBC has a class forcing extension that is pointwise definable:


* *Hamkins, Joel David; Linetsky, David; Reitz, Jonas*, [**Pointwise definable models of set theory**](https://doi.org/10.2178/jsl.7801090), J. Symb. Log. 78, No. 1, 139-156 (2013). [ZBL1270.03101](https://zbmath.org/?q=an:1270.03101).


