A definition of the generic real coded by a generic filter?

Question

Apologies if this question is a bit simplistic/vague for MO:

I'm looking for an all-purpose definition in the literature of when a sufficiently generic filter "canonically codes" a generic real. Examples of what I mean come from everyone's favorite notions of forcing to add certain reals "on purpose":

In Cohen forcing, the generic real is obtained by taking the union of the generic real.

In random forcing, the generic real is obtained by taking the intersection of the generic filter.

In Mathias or Laver forcing, the generic real is obtained by taking the union of stems in the generic filter.

In Sacks forcing, the generic real is obtained by taking the intersection of (branch spaces of trees in) the generic filter... etc, etc.

What I am not looking for is anything having to do with the "other" reals that are added "by accident" through such forcing.

I can, of course, come up with a bespoke definition that covers the above cases, but I was hoping for something general and known.

Edit: To be more precise, I am looking for something that is an injective function from (sufficiently generic) filters to reals. A preliminary definition might be something like: "there is a definable (from the poset $\mathbb{P}$) injection from generic filters for $\mathbb{P}$ to reals". In the case of Cohen forcing, the function would be the map which just takes the union of the generic filter.

Answer 1

In the examples that you gave, the question whether you take a "union of stems" or "intersection of conditions" is really just a matter of notation.

For example, there are several ways to define conditions in Silver forcing: as partial functions from $\omega$ to $2$ with coinfinite domains, or as sufficiently uniform Sacks trees. To get the generic real, you have to take a union of condition in the former case, a union of stems in the latter. And if you identify trees with the corresponding closed set, the generic real will be the unique element of a certain intersection.

In general (not in full generality, but in many cases, in particular: all cases that you mentioned):

• there is a canonical way to associate to each condition $p$ a closed (or at least Borel) set $[p]$. (More precisely, a Borel code for a set.)
• In each of these cases, the intersection $\bigcap_{p\in G} [p]$ will contain a unique element, the generic real $r_G$. (Again, to be precise one would have to talk about Borel codes.)
• The map $G \mapsto r_G$ is (at least in all case considered) 1-1.

Answer 2

Restricting to proper notions of forcing, we have the following (occasionally convenient) characterization of when $\mathbb{P}$ adds a new real,

Proposition: Assume $\mathbb{P}$ is a proper notion of forcing. Then, $\mathbb{P}$ adds a new real, if and only if, for every countable $M\prec H(\theta)$ with $\mathbb{P} \in M$, any $p \in \mathbb{P} \cap M$, every $(M,\mathbb{P})$-generic $q\le p$, and any $q_0 \le q$,

• There exists $G_0, G_1\in Gen_p(M, \mathbb{P})$ such that

  1. $G_0 \neq G_1$, and
  2. $(\forall p_0 \in G_0 \cup G_1)$ $(p_0 \not\perp q_0)$

(where $\,Gen_p(M,\mathbb{P}) \subset [M\cap \mathbb{P}]^{\omega}$ is the set of all maximal $(M,\mathbb{P})$-generic filters $G$, with $p\in G$.)

Proof: The forward direction is easy, the reverse direction requires observing that for every countable $M_0\prec H(\theta)$ with $M \in M_0$ and mutually $(M,\mathbb{P})$, $(M_0, \mathbb{P})$-generic condition $q\le p$, we have $q \Vdash \check{M}\cap G\in \check{M}_0[G] \prec H(\check{\theta})[G]$. $\square$

Corollary: If $\mathbb{P}$ is proper and adds a real, then, $1_\mathbb{P} \Vdash (\exists\,\mathbb{P}_0 \in [\,\mathbb{P}\,]^{\omega}\cap V)(\dot{G} \cap \mathbb{P}_0 \not\in V)$.

---

In light of this Corollary and the examples you provided; if $\mathbb{P}$ is proper, then the only reasonable interpretation of the statement "canonically-codes a generic real" is that there is a countable, definable subset $\mathbb{P}_0 \subset \mathbb{P}$ such that $1_\mathbb{P} \Vdash \check{\mathbb{P}}_0 \cap \dot{G} \not\in V$.

Answer 3

Theorem 1.1 in Golshani's https://arxiv.org/abs/1611.02694 claims that a non-trivial forcing $P$ adds a real $x$ satisfying $V[x]=V[G]$ iff the corresponding CBA $RO(P)$ is countably-generated. One may wonder, if $RO(P)$ is such, whether any complete subalgebra of it has this property, too.