# What is the definition of a Cohen real?

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.

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]$$).
• Thank you for your answer. Sorry if it's a weird question, but is a Cohen real not $(Fin(\omega, 2), \supseteq, 0)$ but $(Fin(\omega, 2), \subseteq, 0)$? I comprehend the order of $(Fin(\omega, 2), \supseteq, 0)$ is the reverse order of the inclusion relation. May 21, 2023 at 3:10