If we say that an effectively generated first order theory $\sf T$ extends $\sf ZF$, such that every countable model of $\sf T$ doesn't have a class forcing extension that is pointwise definable. Would that just mean that $\sf T$ negates Choice? Or it does impart $\sf T$ proving some large cardinal property?



If a theory speaks of sets that cannot be forced to be parameter free definable, then does this entail a large cardinal property?
If $T$ is a theory which proves "there is no extension of the model to a model of $\sf ZFC$ without adding ordinals", then there is no extension of models of $T$ by a class forcing to a pointwise definable model, since pointwise definable models must satisfy $\sf ZFC$.


The obvious example is Gitik's model, but we also have the Morris model where no large cardinals are involved, and for every $\alpha$ there is a set $A\_\alpha$ which is the countable union of countable sets and $\mathcal P(A\_\alpha)$ surjects onto $\omega\_\alpha$. If we extended the Morris model to a model of $\sf ZFC$, then all the $A\_\alpha$ became countable and all their power sets became the same size and therefore proper classes.


