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:
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:
- 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)
- If not in general, are there useful conditions which make it work?
- 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.