Is it consistent with $\sf ZFC + \text{ countable models of } ZFC \text { exist}$, that every countable model of $\sf ZFC$ is a subset of some parameter free definable pointwise-definable model of $\sf ZFC$?



Is every countable model of ZFC a subset of some parameter free definable pointwise-definable model of ZFC?

> 
> The answer is in the positive. Since by the completeness theorem the existence of a countable model of ZFC is equivalent to Con(ZFC), the argument below works with the assumption that ZFC + Con(ZFC) is consistent.
> 
> 
> 


Wojowu's answer already points out that the proof of the following fact (S) can be found in the paper [Pointwise Definable Models of Set Theory](https://arxiv.org/abs/1105.4597) (JSL 2013) by Hamkins, Linetsky, and Reitz.


**(S)** Every countable model of ZFC has a (class) generic extension to model of ZFC that is pointwise definable.


[*Historical note:* (S) was asserted with a proof outline in my paper [Models of set theory with definable ordinals](https://www.researchgate.net/publication/220592523_Models_of_set_theory_with_definable_ordinals), which includes a detailed proof of the weaker statement: *every countable model of ZFC has a generic extension in which all the ordinals are parameter-free definable*. The paper of Hamkins-Linetsky-Reitz presents a detailed proof of not only (S), but also of a corresponding result for countable models of GBC].


Note that (S) is a theorem of ZFC (indeed, it is provable in much weaker systems , but that is a different story). It is easy to see that if the theory ZFC + Con(ZFC) is consistent, then so is $T$ = ZFC + Con(ZFC) + V = L. The fact that $T$ includes the statement V = L implies that $T$ has a global well-ordering of its ambient universe and therefore $T$ has definable Skolem functions. This immediately implies that $T$ has a pointwise definable model $M$. Since (S) is a theorem of ZFC, it holds in $M$, and moreover EVERYTHING in $M$ is parameter-free definable. Thus $M$ is a model in which every countable $N$ model of ZFC has a (class) generic extension $N[G]$ such that (1) $N[G]$ is pointwise definable, and (2) $N[G]$ is parameter-free definable in $M$.


