Konig's tree lemma without using axiom of dependent choice

Question

Konig's tree lemma says that, if $T$ is a rooted tree such that has infinitely many nodes where each node has a finitely many successors, then $T$ has an infinite branch.

I think I have a proof (which I believe is a false proof) of this lemma without using axiom of choice. I would appreciate if you could figure out whether I am actually not using axiom of dependent choice, and also which part of my proof is wrong, in case it is wrong.

My attempt: Given such a tree $T$, consider the set $X:=\{S:S\text{ is a subtree of }T\}$. Then there exists $S\in X$ with the following property:

$\blacksquare$ The root of $S$ has infinitely many children. And at each node $t\in S$, if $t$ has infinitely many children, then there exists unique successor $t'$ of $t$ such that $t'$ has infinitely many children.

So we see that $X':=\{S:S\text{ is a subtree of }T\text{ satisfying }\blacksquare\}$ is a nonempty subset of $X$. Pick $S\in X'$. We will find an infinite branch of $S$.

Starting from $t_0\in S$ the root, having chosen $t_n\in S$ with infinitely many children, there exists a unique successor $t_{n+1}$ of $t_n$ such that has infinitely many children. At each step of the recursive construction of $t_n$, we had a unique choice of $t_{n+1}$. And $\bigcup_n t_n$ will be an infinite brach of $S$.

Edit: From the discussion in comments section, I see that I don't have an argument why $X'$ is non-empty. So is it that, without axiom of dependent choice, $X'$ may indeed be an emptyset?

Answer 1

Your proof will not work, as said in the comments, since it is essentially assuming the existence of a branch.

Indeed, it is consistent without the axiom of choice that there is a family of non-empty sets, each finite, $S_n$, such that $\prod S_n=\varnothing$. Classically, this is done with $|S_n|=2$ for all $n$, in which case we get Russell's example about socks and shoes.

Now define the "choice tree" for this family, namely, $\bigcup_{n<\omega}\prod_{k<n}S_k$, or informally choice functions from an initial segment of the family (initial in the enumeration we have).

This will be a finitely splitting tree, since the successors of any node in the tree correspond to the members of $S_n$, where $n$ is the level of the node, but there will be no branch in this tree, since a branch would correspond to an element of $\prod S_n$, which we know is empty.

Interestingly enough, the exact amount of choice you need is that. That is, every countable sequence of (non-empty) finite sets admits a choice function. This is also equivalent to saying that the countable union of finite sets is countable.