How to make countably closed forcing "nice" without choice When working over a model $V$ of $ZFC$, countably closed forcings are extremely nice:

If $\mathbb{P}$ is countably closed, then $V[G]$ has no new $\omega$-sequences of elements of $V$. In particular, countably closed forcing adds no new reals.

This can fail miserably if $V\models ZF+\neg AC$. In particular, it is consistent with $ZF$ that there is an infinite, Dedekind-finite set $X$ of reals. Letting $\mathbb{P}$ be the poset of finite partial injective maps $\subseteq\omega\rightarrow X$, we have the peculiar result that $\mathbb{P}$ is countably closed inside $V$, since there are no countably infinite subsets of $X$! 
The general question is: without $AC$, what are good ways to tell that forcing with a given poset adds no new reals?
A particular sub-question, that I am separately interested in: if $W\models ZF$, $W$ is an inner model of $V\models ZFC$ with $\mathbb{R}^V=\mathbb{R}^W$, and $\mathbb{P}\in W$ is countably closed in $V$, then forcing with $\mathbb{P}$ over $W$ adds no new reals. However, I don't actually know any ways of building pairs $(V, W)$ with these properties. So, my subquestion is:
How does one show (without extra consistency strength, so not $L(\mathbb{R})$) that there are models $V$ and $W$ of $ZFC$ and $ZF$ respectively, such that $W\models$ "The reals are not well-ordered" and $\mathbb{R}^V=\mathbb{R}^W$?
 A: In Stranger things about forcing without AC,
Comment. Math. Univ. Carolin. 61 (2020),no.1, 21–26, arXiv:1706.01708, Lukas Klausner and I define the combinatorial notion "capstone-closed", which in ZF+DC is equivalent to "$\sigma$-closed", but already in ZF implies "no new $\omega$-sequences" (and also "$\sigma$-closed").
Let $P$ be a partial order. A family $\bar P=(P_n:n\in \omega)$ of disjoint subsets of $P$ is called a pyramid if for all $n\in \omega$ and all $p\in P_n$ there is an $n'>n$ and a condition $p'\in P_{n'}$ which is stronger than $p$. (If you force downwards, as I do, it is really an upside down pyramid, or pıɯɐɹʎd.)
A capstone for a pyramid is a condition $q\in P$ with the following property:

*

*For every $n\in \omega$ there is a condition $p\in \bigcup_{n'>n} P_{n'} $ such that $q$ is stronger than $p$.

(For example, a decreasing sequence of conditions naturally defines a pyramid of singletons, and a capstone for such a pyramid is just a lower bound.)
We call a partial order $P$ capstone-closed if every pyramid in $P$ has a capstone.
To show that a forcing adding a new $\omega$-sequence $\dot f:\omega \to V$ is not capstone-closed, it is enough to consider the sets $P_n$ of all $p\in P$ which decide $\dot f\mathord\upharpoonright n$ but not $\dot f\mathord\upharpoonright (n+1)$
A: This doesn't answer the full version of your question, but it seems pertinent.  
Theorem. (Gunter Fuchs) The following are equivalent over ZF:


*

*DC

*Countably-closed forcing does not add new $\omega$-sequences.
Proof. The forward direction is the usual argument. For the converse, suppose DC fails, so there is a relation $R$ on a set $X$ with no terminal nodes and no $\omega$-sequence through it. Let $\mathbb{P}$ be the forcing notion to add a threading $\omega$-sequence through $R$, consisting of finite sequences $\langle a_0,\ldots,a_n\rangle$, with $a_i\mathrel{R} a_{i+1}$, ordered by extension. The assumption ensures that this forcing is countably closed, for reasons similar to the ones you mention in your question. But the generic filter will create a new threading $\omega$-sequence, since every finite sequence can be extended one more node. QED
A: This is actually a question I am quite concern with at the moment. In its generality, let me give a slight re-hash of what Joel said, with perhaps a slight generalization.$\newcommand{\forces}{\Vdash}$

We say that $\Bbb P$ is $\kappa$-closed if every decreasing sequence of length $\kappa$ (or shorter) has a lower bound. We say that $\Bbb P$ is $\kappa$-Baire (or $\kappa$-distributive) if the intersection of $\kappa$ many dense open sets is dense (and open, trivially).
In $\sf ZF$ we can prove these two theorems:

Theorem I. If $\Bbb P$ is a $\kappa$-Baire forcing then $\Bbb P$ does not add new subsets of size $\leq\kappa$ to the universe.

Proof. Suppose that $p\forces\dot f\colon\check\kappa\to\check V$. By the definition of the forcing relation, for every $\alpha<\kappa$ we have a dense set $$D_\alpha=\{q\leq p\mid\exists x\in V, q\forces\dot f(\check\alpha)=\check x\}.$$
Let $D$ be the intersection of these dense open sets, then by the $\kappa$-Baire property $D$ is dense, and therefore non-empty. Let $q\in D$ then for every $\alpha<\kappa$ there is some $x\in V$ such that $q\forces\dot f(\check\alpha)=\check x$. However $q$ forces that $\dot f$ is a function, therefore this $x$ must be unique. If so the function $g(\alpha)=x$ for which $q\forces\dot f(\check\alpha)=\check x$ is such for which $q\forces\check g=\dot f$, as wanted. $\square$

Theorem II. $\sf DC_\kappa$ holds if and only if every $\kappa$-closed forcing is $\kappa$-Baire.

Proof. Suppose that $\sf DC_\kappa$ holds, the proof goes the same as in $\sf ZFC$. In the other direction, recall that $\sf DC_\kappa$ is equivalent to the following statement:


*

*Every tree $T$ of height $\kappa$, where every sequence of $<\kappa$ has a proper end extension has a branch of length $\kappa$.


Suppose now that $\sf DC_\kappa$ fails, then there is a tree $T$ of height $\kappa$ in which every sequence can be extended, but there is no branch of length $\kappa$. Define $P$ to be the reverse tree order on $T$. This forcing is trivially $\kappa$-closed, because there are no decreasing sequences of length $\kappa$. On the other hand, consider the dense sets $\{q\in T\mid\operatorname{lvl}_T(q)>\alpha\}$. Each is dense open, but their intersection is empty. $\square$

Finally, for real numbers. Or more specifically, sets of ordinals. If a forcing is $\kappa$-Baire then it doesn't add any new sets of size $\kappa$, but we are only interested in sets of ordinals. 
I haven't managed to figure out the exact property, and working with $\kappa$-Baire forcings seems reasonable enough (and controllable enough).
To your subquestion, without verifying the details (I might do so tomorrow, but feel free to let me know if you do it yourself and find a mistake).
Consider the forcing which adds $\aleph_1$ Cohen generics, i.e. $p\in\Bbb P$ is a finite function from $\omega_1\times\omega$ to $2$, with the usual order. Now apply permutations (perhaps with a finite or countable support) of $\omega_1$ onto the left coordinate of the conditions.
Consider the names which are fixed by a countable subset of $\omega_1$. That is to say, there exists $\alpha<\omega_1$ such that whenever $\pi$ fixes pointwise $\alpha$ (as a set), it fixes the name.
I suspect that you can prove that all the real numbers of $V[G]$ enter this symmetric extension (perhaps by some argument that every real number is decided by some countable subset of the forcing, and therefore we can find it a support).
It is easy to show by the usual arguments, though, that there is no well-ordering of $\Bbb R$ in the symmetric extension. 
