Hereditarily Countable Names and Proper Forcing The 'hereditarily countable names' are as defined in Shelah's Proper and Improper Forcing, Chapter 3 Definition 4.1. Let $\mathbb{P}$ be a proper forcing notion and $\dot{Q}$ a $\mathbb{P}$-name such that $\Vdash_{\mathbb{P}}$ "$\dot{Q}$ is a proper forcing notion with set of elements $\check{\kappa}$ and maximal element $\check{0}$".
Let $A$ be the closure of {$\check{\alpha}$ : $\alpha < \kappa$} under the following 2 functions.
(1) given sequences ($p_n$ : $n \in \omega$) and ($\tau_n$ : $n \in \omega$), let $\tau$ be a name forced to be equal to: 
(i) $\tau_i$ where $i$ is the least $n$ satisfying $p_n \in \dot{G_\mathbb{P}}$, if such $i$ exists, and 
(ii) $\check{0}$, otherwise.
(2) given ($\tau_{m, n}$ : $m$, $n \in \omega$), let $\tau$ be: 
(i) the $\epsilon$-least element of $\dot{Q}$ such that for all $m \in \omega$, {$\tau_{m, n}$ : $n \in \omega$} is predense below $\tau$, if such an element exists, and
(ii) $\check{0}$, otherwise.
My question is, is it true that if $p \in \mathbb{P}$ and $\sigma$ is a $\mathbb{P}$-name such that $p \Vdash \sigma \in \dot{Q}$, then there is a $\mathbb{P}$-name $\tau \in A$ such that $p \Vdash \tau \le \sigma$, or even better, $p \Vdash \tau = \sigma$? If so, why is that?
Much thanks in advance.
 A: Counterexample:  Let $\kappa $ be uncountable and let $\mathbb P= \kappa$ be an antichain (with a special weakest element $0_{\mathbb P}$, and let $\mathbb Q$ be forced to be the same forcing. Let $\sigma$ be the $\mathbb P$-name of the generic element of $\mathbb P$. 
Now note that each "hereditarily countable" name uses (hereditarily) only countably many of the names $\check \alpha$, $\alpha<\kappa$.   More precisely:  For every subset $B\subseteq \{ \alpha: \alpha < \kappa\}$ define the family of HC-$B$-names naturally. (That is: all conditions and names appearing in the recursive construction must be in $B$, or HC-$B$-names, respectively.) 
Then show that the set of HC names which are an HC-$B$-name for some countable $B$ is closed under the two operations (1) and (2). 
Every HC-$B$-name for a condition is forced to be equal to the empty condition, or in $B$. 
If the empty condition forces $\tau\le \sigma$ for some HC-$B$-name $\tau$, for some countable $B$. Now choose a condition $p_0\notin B$; then $p_0$ forces that $\sigma=p_0$, but cannot force $\tau=p_0$. 
(I think the point of HC-names is this: If you have a countable set of names $\sigma_n$, and a condition $p$, then you can find a stronger condition $q$ and a set of HC names $\tau_n$, such that $q$ forces $\tau_n \le \sigma_n$  for all $n$. To prove this, let $N$ be a sufficiently large countable elementary model, and let $q$
be generic for $N$. Obtain $\tau_n$ from $\sigma_n$ by ignoring elements outside $N$.) 
