I'm reading about proper forcing for the first time and one of the standard results concerning the properties of $(M,P)$-generic conditions is the fact that in an elementary submodel $M$ of $H_\lambda$ for a large enough $\lambda$ containing $P$ and a name $\dot\alpha$ of an ordinal in
the generic extension $M[G]$ (i.e. $0 \Vdash “\dot\alpha \text{ is an ordinal}"$) then for any $(M,P)$-generic condition $q \in P$ we have $q \Vdash M[\dot G] \cap Ord = M \cap Ord$ where $Ord$ is the set of ordinals in our ground model.
In the proof of this Lemma (see for example Halbeisen, Combinatorial Set Theory, Theorem 21.3), the following set is defined and stated to be open dense
$$D = \left\{ r \in P \mid \exists \beta \in Ord^M: r \Vdash \dot \alpha = \check\beta \right\}.$$
I've been thinking about why this set must be open dense but I have made no progress while also being confused about why this set is not all of $P$ (which my intuition tells me is false) seeing how forcing does not add any new ordinals and $\dot\alpha[G]$ is necessarily one by hypothesis.
Best Answer
One of the ideas behind forcing is that we slowly, but surely, make more and more promises about the generic extensions. And one of the key properties of a promise is that you do not walk back from a promise.
If $\dot\alpha$ is a name and the weakest condition promises it to be a name for an ordinal, then we cannot walk back on this promise. But we also know that at some point, the statements $\dot\alpha=\check\beta$ and $\dot\alpha\neq\check\beta$ will have to be decided. So the set $D$ is the set of all conditions which promise us not only that $\dot\alpha$ will be an ordinal, they specify which one.
The key idea behind properness is that if $M$ is a countable elementary submodel of $H_\lambda$ for a sufficiently large $\lambda$, then the forcing will not add ordinals to $M$ either. It is a condition about how well-behaved a forcing is with respect to countable models. Uri Abraham once explained the idea to me in the most illuminating way:
Being proper simply means that forcing with $P$ commutes with the Mostowski collapse. That is, collapse $M$ to be a transitive model, $\bar M$; take $\bar G$ to be an $(\bar M,\bar P)$-generic filter, where $\bar P$ is the image of $P$, then $\bar M[\bar G]$ has no new ordinals, and if we reverse the transitive collapse and let $G$ be the preimage of $G$, then $M[G]$ should not have new ordinals either. Which is, in its essence, what properness is all about.
Finally, to understand names vs. objects, consider the Cohen forcing with finite partial functions $p\colon\omega\to2$, and let $\dot g$ be the name for the generic function. Now define $\dot m$ to be "the least $n$ such that $\dot g(\check n)=1$", and analyse what each condition force about $\dot m$.
For example, $p$ such that $\operatorname{dom}(p)=\{4\}$ and $p(4)=1$ will force $\dot m<\check 5$, but can it say more than this?