The collection of sets hereditarily definable from the ground model and generic reals

I would like to know whether the following definition of $M$ makes sense.

Let $L$ be an arbitrary (uncountable) set and denote by $\mathbb{C}_L$ the poset that adds a family $C:=\{ c_\ell : \ell \in L\}$ of Cohen reals (i.e. its conditions are finite partial functions from $L\times\omega$ into $\omega$, ordered by $\supseteq$).

In the generic extension $V^{\mathbb{C}_L}$, define $M$ as "the collection of sets hereditarily definable from finite sequences of members of C". In Horowitz and Shelah this seems to be understood as the collection of sets hereditarily definable with parameters in the ground model $V$ and in $C^{<\omega}$. Now I ask:

1. Does this notion of $M$ in Horowitz and Shelah makes sense?

I tend to think it doesn't, in the same way as the class of definable sets is not definable in ZFC. However, I do not see how to justify my suspicions.

2. If the answer to the above is negative, what is the correct interpretation of "the collection of sets hereditarily definable from finite sequences of members of C"?

Considering other references, the natural interpretation would be something like HOD[C] (the collection of sets hereditarily definable from the ordinals and $C^{<\omega}$), but I would like to ask somebody more familiar with this topic to confirm this to me.

Any help will be very appreciated.

• They are indeed using "definable" in the sense of "definable from parameters in $V$ and $C^{<\omega}$". This notion is fine. What precisely makes you think it is not formalizable? – Andrés E. Caicedo Jun 17 '18 at 12:27
• It is just not that clear to me why parameters in $V$ can be used, i.e., how is this formalized (I know it is a beginner's question). Considering Noah's reply below, it seems that the definability of V in the extension is required, isn't it? – dragoon Jun 17 '18 at 23:42
• Sort of. In his paper building a model where all sets of reals are measurable, Solovay explains how to modify the forcing language by adding a predicate for the ground model $V$. This allows us to refer to it and circumvents the problem of definability of $V$ in the extension. – Andrés E. Caicedo Jun 18 '18 at 0:09
• "Considering Noah's reply below, it seems that the definability of V in the extension is required, isn't it?" Yes, but as I explain we do in fact have that, so all is well. (And as Andres explains, even this can be done away with via a bit more work.) – Noah Schweber Jun 18 '18 at 1:10
• It is very clear now. Thanks a lot for your replies. – dragoon Jun 18 '18 at 3:10

This is indeed a reasonable worry to have, since the obvious way to define $M$ is to go through a truth definition for the whole universe, which can't be done. And certainly the class of parameter-freely definable sets can't be defined in a parameter-free way (otherwise, we would be able to express "the least undefinable ordinal").
However, it turns out that there is a trick we can use to talk about definability inside the structure in at least some situations. This is discussed in detail in Kunen's book, in Chapter V.$2$; the crucial ingredient is the Reflection Theorem, which lets us shift from looking for "global" definitions to "local" definitions, and these pose no problem.
This trick only works when ordinals are allowed as parameters; fortunately, this is the case here (note that every ordinal is in $V$). Incidentally, it's worth noting that $M$ is exactly $HOD(V\cup C^{<\omega})^{V^{\mathbb{C}_L}}$ since $Ord\subset V$.
• Thank you for your response. This trick is fine, but don't we require here to use in addition that $V$ is definable (with parameters in $V$) in the generic extension? In your explanation, I don't see clear why $V$ can be replaced by ordinals just like that. – dragoon Jun 17 '18 at 23:44