Proving equivalence of a tree-based version of Countable Choice for families of finite sets.

In this paper by Good and Tree, the following result is mentioned without proof as part of Proposition 6.5:

Each of the following statements imply those beneath it.

The countable union of finite sets is countable.

Every $\omega$-tree has an infinite chain or an infinite antichain.

Every countable collection of [non-empty] finite sets has a choice function.

I know that the first and last statements are equivalent, so that these statements are ostensibly all equivalent. I'm stymied on proving the second implication, though.

I began by taking $\{X_n:n<\omega\}$ to be a countably-infinite collection of finite non-empty sets, putting $X=\bigcup_{n<\omega}X_n,$ and letting $$T=\left\{f\in{}^{<\omega}X:\forall n\in\operatorname{dom}(f)\:f(n)\in X_n\right\},$$ where ${}^{<\omega}X$ is the set of all functions $k\to X$ with $k<\omega$. It is readily shown that $\langle T,\subsetneq\rangle$ is an $\omega$-tree. Now, if the tree has an infinite chain $C,$ then $$B=\bigcup_{f\in C}\{g\in T:g\subsetneq f\}$$ is a branch of length $\omega,$ and $f=\bigcup B$ is readily the desired choice function. On the other hand, if the tree has no infinite chain, then it has an infinite antichain, say $A.$ If $A$ happens to be Dedekind-infinite, then there is a countably-infinite antichain $A'\subseteq A,$ and without loss of generality, we may assume that $A'$ has at most one node on each level. Indexing the elements of $A'$ in order of increasing level by $f_n,$ we define $g(X_k)=f_0(k)$ for $k\in\operatorname{dom}(f_0)$ and $g(X_k)=f_{n+1}(k)$ where $k\in\operatorname{dom}(f_{n+1})\setminus\operatorname{dom}(f_n).$ Then $g$ is the desired choice function, and we're done.

If $A$ is infinite and Dedekind-finite, then...what in the world can be done? We need another (even stronger!) Choice principle to conclude that this is impossible, thereby finishing my proof.

Any hints as to how I can proceed?

Added: To see that the first statement implies the second, suppose we are given an $\omega$-tree $T.$ We know $T$ is countably-infinite since each of its countably-infinitely-many non-empty levels is finite. Let $f:\omega\to T$ a bijection. Supposing that $T$ has no infinite antichain, let $A$ be the set of all nodes of $T$ without successor. Since this is readily an antichain, then it is finite, so, put $$m=\max\bigl(\{0\}\cup\{k<\omega:A\cap T_k\ne\emptyset\}\bigr).$$ Let $c_0\in T_{m+1}.$ Given $c_n$ with height greater than $m$, we have by definition of $A$ and $m$ that $c_n$ has a successor, and letting $$c_{n+1}=f\bigl(\min\{k<\omega:c_n<f(k)\}\bigr),$$ the height of $c_{n+1}$ is greater than that of $c_n$, so also greater than $m$. In this way, we recursively define a strictly increasing sequence of points of $T$, so we have an infinite chain, as desired.

To see that the third statement implies the first, suppose that $\mathcal{A}$ is a countable set of finite sets. For each $A\in\mathcal A,$ we have that $A$ is well-orderable, and in particular can be put into bijection with a unique finite ordinal--namely $|A|.$ There are only finitely-many functions $A\to|A|,$ at least one of which is a bijection, and so the set $B_A$ of bijections $A\to|A|$ is a non-empty finite set for each $A\in\mathcal A.$ Since $\mathcal A$ is countable, then we can therefore use a choice function on $\{B_A:A\in\mathcal A\}$ to choose a bijection $g_A:A\to|A|$ for each $A\in\mathcal A.$ Using these bijections, we can readily show that $$\left|\bigcup\mathcal A\right|\le\sum_{A\in\mathcal A}|A|.$$ Then, since $\mathcal A$ is well-orderable and each $|A|$ is a finite cardinal, then $$\sum_{A\in\mathcal A}|A|\le\max\left\{|\mathcal A|,\sup_{A\in\mathcal A}|A|\right\}\le\aleph_0,$$ whence $\bigcup\mathcal A$ is countable, as desired.

If "Dedekind-finite = finite" holds, then showing the second statement implies the third is simple, but according to the paper, the implication is supposed to hold in $\mathsf{ZF}.$ It's possible that this was simply an error on the authors' part (like leaving off the "non-empty" from the third statement), and that it should specify Dedekind-infinite antichains.

If it is correct, though, then my approach quite simply won't work, since given an arbitrary infinite antichain, it need not have a countably-infinite subset. Certainly any such antichain will be a union of a countably-infinite collection of non-empty finite sets, but it's consistent with $\mathsf{ZF}$ that a countably-infinite union of pairs may be Dedekind-finite.

My question is this: Is it known whether the second statement (as originally written) is equivalent to or strictly weaker than the other two in $\mathsf{ZF}$? If it is equivalent, then can you direct me to a source in which it is proved, or outline an alternate proof technique that does the trick?

[Cross-posted to Math.Overflow.]

Here is a permutation model satisfying:

Form 216: every $\omega$-tree has an infinite chain or infinite antichain

but not

Form 10: countable unions of finite sets are countable

By Pincus’ transfer result [1] this means there is no implication in ZF, unless ZF is inconsistent. Form 216 (plus the negation of Form 217) is actually given as an example of a transferable statement - see 2B5 on page 724 of [1]. My impression is that Form 216 is only of interest for appearing in Pincus’ dissertation, and in this mistake in the Good-Tree paper.

Rather than talk about antichains, for the following arguments it will be easier to obtain a related object: a “nowhere dense” subtree. A subtree of a tree is a downwards-closed subset. A subtree $T_0\subset T$ is nowhere dense if for every $t_0\in T_0$ there is $t>t_0$ with $t\in T\setminus T_0.$ (This is not standard terminology.)

Lemma. Any $\omega$-tree $T$ with an infinite nowhere dense subtree $T_0$ has an infinite antichain.

Proof: Take the antichain $D$ of minimal elements of $T\setminus T_0.$ For each $n,$ there is an element $t_0\in T_0$ of height $n,$ and since $T_0$ is nowhere dense there must be some $t>t_0$ not in $T_0.$ A minimal such $t$ is an element of $D$ of height at least $n+1.$ This shows that $D$ has elements of arbitrarily large heights, which means $D$ is infinite. $\square$

(The reverse implication also holds: given an infinite antichain $D,$ take $T_0$ to be the set of elements $t\in T$ such that there are infinitely many $d\in D$ with $d>t.$)

Enumerate the primes as $p_1,p_2,\dots.$ The set of atoms $A$ has an element $a(n,i)$ for each $n\geq 1$ and each $i\in\mathbb Z/p_n\mathbb Z.$ The group of permutations is the product $G=\prod_n (\mathbb Z/p_n\mathbb Z),$ acting by $\pi(a(n,i))=a(n,i+\pi_n).$ Let $\mathcal S$ be the set of subsets of $\mathbb N$ of zero upper density. For each $S\in\mathcal S$ define the subgroup $G(S)$ of permutations $\pi$ with $\pi_n=0$ for all $n\in S.$

This data $(A,G,\{G(S):S\in\mathcal S\})$ defines a permutation model $N.$ A good reference for permutation models is Jech’s “Set Theory”, but I’ll give a very informal brief description. Working from a model of ZFC, we construct a universe of sets $V$ built from $A$ by the operations of taking power sets and subsets. $V$ is a model of ZFA (ZF with atoms, also known as ZFU) satisfying the axiom of choice. The permutation action of $\pi\in G$ extends to an action on these sets. A set is “symmetric” if there exists $S$ such that $G(S)$ fixes $x,$ so $x=\pi x$ for all $\pi\in G(S).$ We restrict the universe to sets $x$ which are hereditarily symmetric, recursively defined as: $x$ is symmetric, and each element of $x$ is hereditarily symmetric. We don’t require the same $S$ to be used for different elements. This produces the permutation model $N,$ which satisfies ZFA. Existence arguments can be carried out in $V,$ with a verification that the result actually exists in $N.$

The sequence of finite sets $A_n=\{a(n,i):i\in\mathbb Z/p_n\mathbb Z\}$ exists in $N.$ We’ll show that their union is not countable. Given a function $f:\mathbb N\mapsto \bigcup A_n$ fixed by $G(S),$ pick $n\not\in S$ and $\pi\in G(S)$ with $\pi_n\neq 0.$ We cannot have $f(k)=a(n,0)$ for any $k,$ because then $f(k)=(\pi f)(\pi k)=\pi(a(n,0))=a(n,\pi_n)\neq f(k).$ So Form 10 fails in $N.$

A nice feature of this model is that symmetries of finite sets have a simple classification. A highbrow description is that we’re using automatic continuity for a profinite topology. Consider a $S\in\mathcal S$ and an $x\in N$ such that the orbit $G(S)x$ has a finite cardinality $m.$ Let $X$ be the set of indices $n\in\mathbb N\setminus S$ such that $p_n$ divides $m.$ Since permutation actions of abelian groups are regular, the stabilizer is well-defined and has index $m.$ The action therefore factors through $G(S)/mG(S).$ But this group has cardinality at most $m,$ because the second summand below is $m$-divisible so gets included in $mG(S)$: $$G(S)=(\prod_{n\in X} \mathbb Z/p_n\mathbb Z)\times (\prod_{n\in S\setminus X} \mathbb Z/p_n\mathbb Z).$$ The first summand is forced to have order $m,$ which means $m$ is the product of its prime factors, $\prod_{n\in X} p_n.$ The first summand acts freely and transitively, while the second summand acts trivially. Note that $X$ is the unique minimal set such that $x$ is fixed by $G(S\cup X).$

Consider an $\omega$-tree $(T,<)$ in $N$ fixed by some $G(S_T),$ and assume that $T$ has no infinite chain in $N.$ We aim to show that there is an infinite nowhere dense subtree of $T$ in $N.$

Pick an infinite chain $x_0<x_1<\dots$ in $T.$ For $n\in\omega$ let $X_n$ be the unique minimal finite set such that $x_n$ is fixed by $G(S_T\cup X_n).$ These form a non-decreasing chain $X_0\subseteq X_1\subseteq \dots$ because any tree automorphism that moves a parent node must move all its child nodes. Let $X_\infty=\bigcup X_n.$ We cannot be in the situation $X_\infty\in\mathcal S$ because that would imply $S_T\cup X_\infty\in\mathcal S,$ which would mean that the chain $\{x_i:i\in\omega\}$ is in $N.$

Pick any infinite $S\subset X_\infty$ of zero upper density, for example $S=\bigcup_n \min\{i\in X_\infty: i\geq n^2\}.$ I claim that the subtree $$T_0=\{\pi x_i : \pi\in G(S_T\cup S), i \in \omega\}\subset T$$ is nowhere dense. To verify this we need to show that for each $\pi\in G(S_T\cup S)$ and each $i \in \omega$ there exists $t>\pi x_i$ with $t\not\in T_0.$ By applying $\pi^{-1}$ to both sides we can assume $\pi$ is the identity. For large enough $j>i$ there exists $n\in (X_j\setminus X_i) \cap S.$ The action of $G(S_T\cup S\setminus \{n\})$ on its orbit of $x_j$ factors through the group $$H=\prod_{k\in \{n\}\cup (X_j\setminus S)} \mathbb Z/p_k\mathbb Z.$$ $H$ acts regularly on the orbit $Hx_j,$ so the orbit $G(S_T\cup S\setminus \{n\})x_j$ is $p_n$ times larger than $G(S_T\cup S)x_j.$ Pick any $t$ in the former but not the latter, for example $t=\sigma x_j$ where $\sigma_n=1$ and $\sigma_m=0$ for $m\neq n.$

$T_0$ is in $N,$ and it’s an infinite nowhere dense subtree of $T.$ By the Lemma, we have verified that Form 216 holds in $N.$

[1] Zermelo-Fraenkel Consistency Results by Fraenkel-Mostowski Methods, David Pincus, The Journal of Symbolic Logic, Vol. 37, No. 4 (Dec., 1972), pp. 721-743

Upon further research--in particular, upon inspecting the numerical list of forms from Howard and Rubin's "Consequences of the Axiom of Choice"--I noticed that Howard and Rubin's text actually references Good and Tree's paper. I also see that the first statement above readily implies Form 10A from H & R, the second statement above is Form 216 from H & R, the third statement above is Form 10 from H & R, and I give proof in the question that the third statement implies the first, so that the first statement is again equivalent to form 10. Furthermore, I noted that form 10F from H & R is the following:

Every $\omega$-tree has an infinite chain.

This clearly implies the second of G & T's statement above, and I suspect that it is what was intended by G & T, in the first place. Most notably, according to this site, H & R's text cites that Form 10 is stronger than Form 216, but that it was not known to be strictly stronger. This leads me to suspect (even more strongly) an error on G & T's part. Obviously, if it holds in $\mathsf{ZF}$ that every $\omega$-tree with an infinite antichain must have an infinite chain, then it isn't strictly stronger, but I'm unable to prove this or find any information confirming/denying this, so I suspect that it is an open question.

One thing I was able to find is that Keremidis published a proof (in Mathematica Japonica, Vol. 51, No. 2, pp. 175-178) that Form 9 from H & R (Every Dedekind-finite set is finite.), which is strictly stronger than Forms 10 and 216 in $\mathsf{ZF}$, is equivalent to the following statement: