Forcing $\neg\square_{\omega_1}$ from a Mahlo cardinal, reference

Question

In Jensen's The fine structure of the constructible hierarchy, it is stated that Solovay proved the consistency of $\neg\square_{\omega_1}$ by collapsing a Mahlo cardinal to $\omega_2$. I was wondering where I can find a proof of this result.
Thanks

Answer 1

I'll give the proof, which was told to me by Martin Zeman.

Let $G \subseteq \mathrm{Col}(\omega_1,{<}\kappa)$ be generic, where $\kappa$ is Mahlo. Suppose towards contradiction that $\square_{\omega_1}$ holds in $V[G]$, let $\mathcal C$ be a square sequence, and let $\dot{\mathcal C}$ be a name for it. By the $\kappa$-c.c., there is a club of $\alpha<\kappa$ such that $\mathcal C \restriction \alpha$ is computed in $V[G \restriction \alpha]$. By Mahloness, let $\mu<\kappa$ be such a point that is inaccessible in $V$. So $\mu = \omega_2^{V[G \restriction \mu]}$, and $\mathcal C \restriction \mu$ is a square sequence in $V[G \restriction \mu]$.

Now in $V[G]$, $\mathcal C \restriction \mu$ gets threaded by $\mathcal C(\mu)$, and $\mu$ has cofinality $\omega_1$ in $V[G]$. But it is easy to show that there is only one thread, so it is definable whenever it exists. (This seems to me to be a curious example that may go against some philosophical intuitions, a mathematical object that is uniquely definable, but may or may not exist. Please give your thoughts in the comments! ;-P)

Finally, the tail of the forcing, $\mathrm{Col}(\omega_1,{<}\kappa)/ (G \restriction \mu)$, is homogeneous. Since $\mathcal C(\mu)$ is a subset of $\mu$ definable from a parameter from $V[G \restriction \mu]$, general facts about homogeneous forcing show that it is an element of $V[G \restriction \mu]$. (Definable as the set of $\alpha<\mu$ such that $1 \Vdash \alpha \in \dot{\mathcal C}(\mu)$.) But this means $\mu$ is collapsed to $\omega_1$ in $V[G \restriction \mu]$, which is false because $\mathrm{Col}(\omega_1,{<}\mu)$ is $\mu$-c.c.