What is the definition of a Cohen real?

Question

When I study set theory research, I sometimes come across "Cohen reals"(such as Joel David Hamkins' paper). However, I can't have found the definition of Cohen reals. What I know about Cohen forcing is: Given the partially ordered set $(Fin(\omega, 2), \supseteq, 0)$ that is the poset of all finite functions from $\omega$ to $2$ (or a subset of $\omega$), let $G'$ be a generic filter for this poset($'$ represents that its generic filter is strictly different with the generic filter below). Then, $g = \cup G'$ is a well-defined total function(so is seen as a real number such as $0.1001011110...$) which doesn't exist in the ground model $V$. Then, in order to get $\omega_2$ new total functions, one can replace $\omega$ by $\omega \times \omega_2$ and (since this poset satisfies the countable chain condition) is given the forcing extended model $V[G]$ that doesn't satisfies the continuum hypothesis(if there are errors the above, could you tell me). Does Cohen reals appear in the above? Or is it a different object? I'd appreciate it if you could answer the question.

Answer 1

A Cohen real is a real which is generic for Cohen forcing $\mathbb{C}=(Fin(\omega,2),\supseteq,0)$. Strictly speaking of course this depends on the choice of ground model: if $M$ is a countable transitive model of $\mathsf{ZFC}$ then there will exist (in $V$) a Cohen-over-$M$ real $r$, but $r$ is obviously not Cohen over $M[r]$.

In the usual argument for the failure of $\mathsf{CH}$, for example, the "rows" of the generic function $\omega\times\omega_2^M\rightarrow 2$ are indeed Cohen reals (over the original ground model $M$), and the forcing used has "added $\omega_2^M$-many Cohen reals."

It's worth noting that adding a single Cohen real does not actually add a single Cohen real. Less elliptically, if $r$ is Cohen-over-$M$ then $M[r]$ contains lots of reals that are also Cohen-over-$M$. For example, the real $s(x)=r(2x)$ (basically, "half" of $r$ itself) is a Cohen real and generates a strictly smaller extension $M\subset M[s]\subset M[r]$. Similarly, it is generally a difficult problem to determine whether a forcing notion adds a Cohen real (precisely: given $M$ and $\mathbb{P}$, determine whether for every $\mathbb{P}$-generic-over-$M$ filter $G$ there is a Cohen-over-$M$ real $r\in M[G]$).