# iterate random forcing

I am studying Kunen's article Random and Cohen forcing [1], and I meet a problem. On page 904, Theorem 3.13 states that if $M$ is a countable transitive model of ZFC, $I,J,K \in M$ such that $I$ is a disjoint union of $J$ and $K$, and $F \in 2^{I}$ is null-generic over $M$ (i.e. a random real), then the restriction of $F$ on $K$ is generic over $M[F|J]$ (that is (2)).

He proved this by letting $r$ be a name for random reals. Then he said there is a formula $\psi(r)$ which represents "$r|K$ is generic over $M[r|J]$". What does $\psi$ looks like? I don't know how to write "$r_{F}|K$ is generic over $M[r_{F}|J]$" as a formula in $M[F]$, could anybody help me?

Bibliography: (Added by A.K.)

1. Kenneth Kunen. Random and Cohen Reals. Handbook of Set–Theoretic Topology, pp 887–911. Elsevier Science Publishers B.V., 1984.
-
I have added the reference to the article, so people can look it up more easily. –  Asaf Karagila Oct 23 '11 at 13:08
Sounds like you need a reference to Solovay's theorem (in Kanamori's "The Higher Infinite" 10.21). –  Eran Oct 29 '11 at 14:42

$\psi(r)$ could say: "For every Baire null $B \subseteq 2^{K}$ coded in $M[r|J]$, $r|K \notin B$". This formula uses the set of codes for Baire subsets of $2^K$ in $M[r|J]$ as a parameter.