Solution (source code)

= Solution

Write $\mathcal T(D)$ for the <recursively repetition-free labelled trees>. Each <rooted tree> is finite because the inductive definition forms it from an already constructed finite list of finite child <rooted trees>. Its label list is obtained by visiting the root first, then each child subtree in its prescribed order, using a <depth-first traversal of a tree>. This list can have repetitions. In particular, different branches may use the same label; the children are required to be distinct <rooted trees>, not to have distinct root labels.

For any finite label pool $F$, prove by <mathematical induction> on $|F|$ that $\mathcal T(F)$ is finite. For $F=\varnothing$ it is empty. For each root $d\in F$, the children form a <finite repetition-free sequence> from $\mathcal T(F\setminus\{d\})$, which is finite by <mathematical induction>. There are therefore finitely many child lists for that root, and the finite union over $d\in F$ is finite. More explicitly, if $t_m$ is the number of <rooted trees> on a pool of $m$ labels, then
$$
t_0=0,\qquad t_m=m\sum_{k=0}^{t_{m-1}}\frac{t_{m-1}!}{(t_{m-1}-k)!}.
$$
There is no countable choice in this finite <mathematical induction>.

Now suppose $T_0,T_1,\ldots$ were an injective enumeration of a countably infinite subset of $\mathcal T(D)$. Their canonical traversal lists give an explicit enumeration of all labels used. If infinitely many different labels occur, the least-first-occurrence procedure gives a countably infinite subset of $D$, a contradiction. Otherwise all labels belong to one <finite set> $F$. Every $T_n$ then belongs to $\mathcal T(F)$: recursively its root lies in $F$ and its child <rooted trees> use only $F$ with that root removed. But $\mathcal T(F)$ is finite by the preceding <mathematical induction>, again a contradiction. Finally $d\mapsto$ the single-vertex <rooted tree> labelled $d$ is injective, so $\mathcal T(D)$ is infinite. Hence <recursively repetition-free labelled trees preserve Dedekind-finiteness>:
$$
\boxed{\mathcal T(D)\text{ is an infinite Dedekind-finite set.}}
$$