@Lorenzo: I don't know, is the simple answer! I imagine that the answer is positive, since the forcing in not ccc, and we can do some crazy diagonalisation thing where we evade any Cohen dense set from the ground model. But I haven't got the slightest idea as to how to actually prove that.

@Noah: You can find it, in a nutshell, in mathoverflow.net/q/110799/7206, with the added step that this time we do this forcing over $V_\kappa$, so it's not a class forcing from out perspective.

Depending on your preexisting knowledge, Jech might be good. Or Enderton. Or Just & Weese. You can take a look on my website, there are lecture notes in set theory which briefly touch on $L$. After reading those, Jech would probably be a suitable option.

Yes. That is what I'm saying. $V_{\kappa+1}$ is the set of all the subsets of $V_\kappa$, and since $V_\kappa\times V_\kappa\subseteq V_\kappa$, it also contains all the functions and relations on $V_\kappa$. Apply the $\sf C$ in your $\sf ZFC$ and you're done. As for the $L$ notation, this is Gödel's constructible universe which is constructed by taking the definable power set instead of the full power set at each stage. If you're unfamiliar with that, feel free to ignore it, consider it a blackbox, or learn more set theory to be more familiar with it! :-)

@Noah: I mean, the first one is truly trivial. Picking two maps. We can easily lift them to maps from the product...

I'd hazard a guess that this wasn't really known, or at least never explicitly stated. I certainly didn't know that before Elliot Glazer told me about it.

Vaguely related is my work with David, Sean, and Christoph on $\kappa$-Strongly Proper forcings.

@Gabe: Boban asked me back in 2018, if the ZF large cardinals are so interesting, how come nobody works on that? My answer was that in the past couple of decades Hugh was "just about to disprove it". I feel that this had been a significant reason nobody worked on this for the past 30 years or so.

I think if you look at the HOD Conjecture as a sort of covering lemma, things kind of make sense. And if you think about HOD as a second-order constructible universe, then it kind of makes sense that this connects to cardinals that are strongly associated with second-order logic (i.e. supercompactness and extendible cardinals). I can understand why Hugh would conjecture the HOD Hypothesis is provable (from certain assumptions), although we never discussed that specifically. It's just about what sort of structure and restrictions you expect the universe to have.

arxiv.org/abs/2010.15632 :-)

@Gro-Tsen: The rational numbers are well-orderable.

But is it a spherical cow in vacuum?

Assuming $2^{\aleph_0}=2^{\aleph_1}$ we get that $|W(\omega)|=|W(\omega_1)|$.

@Joel: Going by Lorenz's book, you're assuming that Mathias forcing is defined only with a Ramsey family, rather than an arbitrary filter? I think we're talking past each other using the same language with different meaning.

@Joel: Oh. So the pairs are just $(s,A)$ where $s$ is a finite sequence and $A$ is a positive measure (with respect to the filter)? In this case I vaguely remember a dichotomy: either the forcing is ccc or else it collapses the continuum.