Existence and uniqueness of Borel-code evaluation

On any function $h$ on the children of $s$, replace values not in $\mathcal{P}(X)$ by $\mathrm{\varnothing }$, then apply the operation specified by the label at $s$. This is a definable, single-valued, total rule returning a subset of $X$. The child relation is well-founded by F1 and setlike because $T$ is a set. F2 therefore supplies a set function $E$ on $T$ satisfying the rule. Every value is a subset of $X$, so no replacement of an actual value occurs, and the displayed equations hold.

If $E^{\mathrm{\prime }}$ is another evaluation agreeing with $E$ at the children of $s$, the relevant union, complement, or fixed leaf value is identical, so $E^{\mathrm{\prime }}(s)=E(s)$. This property is progressive, and F3 proves equality at all nodes. For Borelness, leaves are basis opens, a complement of a Borel set is Borel, and a union node uses the sequence indexed by $k\in \mathbb{N}$, filling absent children by $\mathrm{\varnothing }$. Borelness is therefore progressive too; F3 proves it at every node.

Let $\mathcal{H}$ be the set of root values of valid codes. A single leaf codes each $U_n$. For any open $V$, give a union root one child $(n)$ labelled leaf$(n)$ for each $n$ such that $U_n\subseteq V$. Its evaluation is $\bigcup \{U_n:U_n\subseteq V\}=V$ by the basis property. This includes $V=\mathrm{\varnothing }$ and an empty union. The tree has height at most one and hence is well-founded: a nonempty subset containing a child has that child minimal; otherwise its root is minimal.

From a code $(T,l)$ for $B$, form $T^{\mathrm{\prime }}=\{\mathrm{\varnothing }\}\cup \{(0{)}^{⌢}s:s\in T\}$, put a complement label at its root and copy all other labels. It codes $X\setminus B$. For a sequence $(B_n)$ in $\mathcal{H}$, the sets of codes for the respective $B_n$ are nonempty subsets of the one set of all labelled trees. A1 selects $(T_n,l_n)$ for all $n$. The tree $T^{\mathrm{\prime }\mathrm{\prime }}=\{\mathrm{\varnothing }\}\cup \{(n{)}^{⌢}s:n\in \mathbb{N},s\in T_n\}$, with union root and inherited labels, codes ${\bigcup }_n{B}_n$.

Both graftings in step 2.3 are well-founded. Given a nonempty subset meeting a tagged constituent subtree, take a minimal element of its intersection with that one subtree. Every child of that element is still in that subtree, so it is minimal in the whole subset. If no constituent subtree is met, the subset consists of the root. Thus the graftings are valid codes. By steps 2.2–2.3, $\mathcal{H}$ contains all opens and is closed under complement and countable union; it therefore contains $\mathcal{B}(X)$. Step 2.1 gives the reverse inclusion. This proves the converse under AC and completes the claims, including $X=\mathrm{\varnothing }$. QED.