Well-ordering the reals: finding a certain model of $\mathsf{ZFC}$

Question

How would one go about constructing a model $\mathfrak{M}$ of $\mathsf{ZFC}$ such that under $\mathfrak{M}$, no formula defining a well-ordering of $\mathbb{R}$ exists? I am certain such models are present in the literature but I am having trouble finding any references to them.

Answer 1

If $M$ is a countable transitive model of $\text{ZFC}$, $\mathbb{P}$ is finite support $\omega_1^M$ product of Cohen forcing, and $G$ is a $\mathbb{P}$-generic over $M$, then $\text{HOD}_{({}^{\omega}\omega)^{M[G]}}^{M[G]}$ is a model where the reals can not be well-ordered. The verification requires some understanding of forcing and the hereditarily ordinal definable sets.

Basically, the idea is to find a forcing extension where the reals do not have an ordinal definable embedding into the ordinals. Then consider the model of hereditarily ordinal definable sets using the reals as parameters.

The end of chapter 14 in Jech $\textit{Set Theory}$ has a detail proof that shows such a model (using a different forcing) works.