One of the first forcing facts that we learn is that -closed forcings preserve all sequences of length . This is usually shown via distributivity, by showing that every -closed forcing is also -distributive, and that -distributivity is *equivalent* to the forcing not adding any new sequences of length . I will recall these facts here, and show how they relate to both and . Here is the axiom of choices, stating that we have choice functions for all sets injecting into , and is the axiom of dependent choices, saying that every pruned tree of height at most has a branch.

Let’s start off by recalling a few definitions of the terms I just mentioned. I’ll be slightly unorthodox here and follow the convention in both Jech (1999) and Schindler (2014) that -closed and -distributive are referring to sequences of length . Others might denote this by -closed and -distributive, respectively.

Definition.Let be an infinite cardinal and a forcing. Then is…

-closedif every -descending chain of conditions has a lower bound ; i.e., holds for every .-distributiveif the intersection of every -sized collection of open dense subsets of is again open dense.

The following is the well-known reason for why we care about distributivity.

Lemma 1 (ZF).Let be an infinite cardinal and a -distributive forcing. Then doesn’t add any new -sequences.

**Proof.** Let be -generic and fix any such that ; say for a set . Fix forcing that and define, for each ,

,

all of which are open dense, so -distributivity of implies that is open dense as well; let . Since we get for each a unique with . We can therefore define, in , as the function given as , so that . **QED**

In many circumstances we’d simply show that our forcing of choice is -closed however, when we want to show that it doesn’t add any new -sequences. But this implication turns out to require some amount of choice, which is the following folklore result:

Proposition (ZF).Let be an infinite cardinal. Then the following are equivalent:

- Every -closed forcing is -distributive
- Every -closed forcing does not add any new -sequences.

**Proof.** Lemma 1 above gives us .

: Let be -closed and fix a -sequence of open dense subsets of . Let and use to find a -sequence with and for every . Since is -closed we get a with , showing -distributivity.

: Assume fails, so that there’s a pruned tree of height without any branch. As a forcing, is then trivially -closed. But if is any generic then is a branch through and therefore contains a new -sequence. **QED**

Okay, so it seems that there’s some nontrivial stuff going on between the distributivity and the closure, and the proposition seems to indicate that we also get the converse of Lemma 1 in ZF. This at least holds if we’re assuming separativity and some choice:

Lemma 2 ().Let be an infinite cardinal and a separative forcing. Then is -distributive iff it doesn’t add any new -sequences.

**Proof. ** is just as above, so we show : Let be a sequence of open dense subsets of and fix some ; we have to show that there’s a with . Let be a -generic filter with . In we may then form the sequence

,

all of which are nonempty. Now use to pick a sequence of conditions . By assumption this sequence also belongs to so that we can then define, in , the set

,

which is dense below by separativity of , so pick . Since for every , as they’re all elements of , we get that for every . Since was arbitrary we get that is dense, showing -distributivity. **QED**

Note that we need the separativity assumption, as otherwise we could let and , which doesn’t add any new sequences (or any sets at all, in fact), but it isn’t -distributive.

If we assume some stronger condition on our forcing we *can* get the equivalence in ZF, however:

Lemma 3 (ZF).Let be an infinite cardinal and a separativetree forcing; i.e., where every compatible pair is also comparable. Then is -distributive iff it doesn’t add any new -sequences.

**Proof.** This is exactly like the proof of Lemma 2, but we have to *construct* the sequence of ‘s instead of relying on choice. Again we have, in , the sequence

,

all of which are nonempty. Note that every pair of is compatible, being elements of the filter, so they are comparable as well as is a tree forcing. This makes a branch, which is then wellordered by ‘s ordering . Define the sequence as

,

and finish the proof as in Lemma 2. **QED**

The general question of whether the converse of Lemma 1 holds in ZF seems to be open though, so let’s state it here for convenience:

Open problem? (ZF)Let be an infinite cardinal and a separative forcing which doesn’t add any new -sequences. Is then -distributive?

**Update: **This might have a positive answer, by @PBL05240969‘s argument in this Twitter thread.