# Class Forcing and Genericity: Predense sets vs Dense classes

In short my question is: why do we use definable classes in the definition of genericity for class forcing, instead of predense sets.

To elaborate, in Sy's book and indeed other sources on the subject of class forcing, $G$ is generic if it meets every definable, dense class of $M$, the ground model; a natural extension of the usual situation. Of course classes can get a bit tricky so one would naturally wonder whether one can use predense sets in their place: intuitively the answer should be "no," since otherwise we'd probably go ahead and do so. Indeed, Stanley outright says that this "definable genericity" is stronger than "internal genericity" [1].

Thus my question is really twofold:

1. What is the problem with the standard argument that genericity defined for predense sets is the same:

Let $\mathbb P$ be a definable class forcing. Let $D$ be a predense set of $M$, let $\tilde D$ be the class of extensions of $D$, which is definable ($\tilde D=\{p\in\mathbb P\mid \exists q\in D(p\leq q)\}$) and dense (as usual: if $p\in\mathbb P$ then there is a $q\in D$ compatible with $p$, hence an $r \in \tilde D$ extending $q$.) So by definable genericity, there is $r\in G\cap\tilde D$, which must come from extending a $q\in D$, which is also in $G$ since it's a filter.

I assume I'm doing something naughty with those proper classes, but I don't see where.

So, with a little more thought it's obvious that it's the other direction that's the issue, i.e., if $G$ is internally generic, when is it definably generic. Thus I would like to know about this with respect to the pretameness condition that Sy defines:

$\mathbb P$ is pretame iff given a $p$, any $M$-definable sequence of dense classes can be refined to a sequence (in $M$) of predense sets below some $q\leq p$.

so:

2. Does class forcing work out OK if we use predense sets? Can the extension satisfy ZFC(-) (in the language with a predicate for the generic)

3. If not in general, are there useful conditions which make it work?
4. What are some examples of cases where the difference matters?

I'm actually most interested in the situation of Prikry forcing over a model with an $M$-ultrafilter.

[1] Stanley, M.C., 2003, Outer Models and Genericity. JSL.

Let me point out that meeting all pre-dense sets is not generally the same as meeting all dense classes. Consider the forcing $\mathbb{P}$ that adds a generic function from $\text{Ord}$ to $V$. (One can use this forcing to force global choice — see Victoria Gitman's account.) That is, conditions are functions $p:\alpha\to V$ for some ordinal $\alpha$, and the order is extension of functions. If a filter $G\subset\mathbb{P}$ meets all dense classes, then it is easy to see that $\cup G$ is a surjective function total function from $\text{Ord}$ to $V$: for any set $x$, it is dense that the conditions have $x$ in their range, and for any ordinal $\alpha$, it is dense that the conditions are defined at $\alpha$.
But that argument breaks down completely if one tries to use only predense sets: the reason is that the forcing $\mathbb{P}$ has no pre-dense sets at all! (except for sets that contain the empty function) For any set $B$ of nontrivial conditions, there is a condition $p$ that is incompatible with every element of $B$. So it turns out that every filter vacuously meets all pre-dense sets, and the forcing technology would not be doing what we want.
One can transform $\mathbb{P}$ into forcing that also adds sets, for example, by using the generic filter to determine what happens next, for example, to code $G$ into the GCH pattern.