The tree and successor-menu formulations of DMC are equivalent

Assume the tree form of the statement.

Assume the successor-menu form of the statement.

Under step 1.1, let $A$ be a nonempty set and let $R$ be serial on $A$; the $R$-chain tree $T_R$ is a pruned tree of height $\omega$ with nonempty levels, so by the tree form there is a subtree $T^{\mathrm{\prime }}$ of $T_R$ whose levels $T_n^{\mathrm{\prime }}$ are nonempty and finite.

Under step 1.2, let $T$ be a pruned tree of height $\omega$ on a set $A$ with nonempty levels, and let $R\subseteq T\times T$ be the relation of immediate succession, $tRu$ exactly when $u=t^{⌢}a$ for some $a\in A$.

Under step 2.1 the given subtree $T^{\mathrm{\prime }}$ need not be pruned, so prune it first: put $T^{\mathrm{\prime }\mathrm{\prime }}:=\{t\in T^{\mathrm{\prime }}:\text{for every }j>\mathrm{dom}t\text{ there is }v\in T_j^{\mathrm{\prime }}\text{ with }t\subseteq v\}$. Then $T^{\mathrm{\prime }\mathrm{\prime }}$ is a subtree of $T_R$ contained in $T^{\mathrm{\prime }}$ (it contains the empty sequence, since $T^{\mathrm{\prime }}$ has nonempty levels, and it is closed under initial segments, since a shorter initial segment of $t\in T^{\mathrm{\prime }\mathrm{\prime }}$ is extended by the same nodes that extend $t$), and each level $T_n^{\mathrm{\prime }\mathrm{\prime }}\subseteq T_n^{\mathrm{\prime }}$ is finite. Each level $T_n^{\mathrm{\prime }\mathrm{\prime }}$ is also nonempty: otherwise every $t\in T_n^{\mathrm{\prime }}$ would have a least level $j(t)>n$ with no extension in $T^{\mathrm{\prime }}$, and with $j^{\ast }:=\max \{j(t):t\in T_n^{\mathrm{\prime }}\}$ (a maximum over the finite set $T_n^{\mathrm{\prime }}$, whose members are naturals) no node of $T_{j^{\ast }}^{\mathrm{\prime }}$ extends any member of $T_n^{\mathrm{\prime }}$, although every $v\in T_{j^{\ast }}^{\mathrm{\prime }}$ is an extension of $v\upharpoonright n\in T_n^{\mathrm{\prime }}$. Finally every node $t\in T_n^{\mathrm{\prime }\mathrm{\prime }}$ has an extension in $T_{n+1}^{\mathrm{\prime }\mathrm{\prime }}$. If a one-step extension in $T_{n+1}^{\mathrm{\prime }}$ already belongs to $T^{\mathrm{\prime }\mathrm{\prime }}$, there is nothing to prove. Otherwise suppose every one-step extension of $t$ in $T_{n+1}^{\mathrm{\prime }}$ lies outside $T^{\mathrm{\prime }\mathrm{\prime }}$; their set $B$ is nonempty because $t\in T^{\mathrm{\prime }\mathrm{\prime }}$, and it is finite as a subset of $T_{n+1}^{\mathrm{\prime }}$. Each $u\in B$ has a least dying level $j(u)>n+1$ with no extension in $T^{\mathrm{\prime }}$. Put $j^{+}:=\max \{j(u):u\in B\}$. Since $t\in T^{\mathrm{\prime }\mathrm{\prime }}$, take $w\in T_{j^{+}}^{\mathrm{\prime }}$ extending $t$, and let $u_0:=w\upharpoonright (n+1)$. Then $u_0\in B$ by the supposition, but $w$ gives an extension of $u_0$ through its dying level $j(u_0)\le j^{+}$, a contradiction. Now put $F_n:=\{t(n):t\in T_{n+1}^{\mathrm{\prime }\mathrm{\prime }}\}$, the set of last entries of the nodes of $T^{\mathrm{\prime }\mathrm{\prime }}$ of length $n+1$: each $F_n$ is nonempty and finite, and if $x\in F_n$ is the last entry of $t\in T_{n+1}^{\mathrm{\prime }\mathrm{\prime }}$ then $t$ has an extension in $T_{n+2}^{\mathrm{\prime }\mathrm{\prime }}$, so $x$ has an $R$-successor in $F_{n+1}$, namely the last entry of that extension.

Under step 2.2: the relation $R$ is serial on $T$, because $T$ is pruned and every proper extension of a node of length $n$ passes through an immediate successor in $T$ by [F2]; the set $T$ is nonempty, since it contains the empty sequence.

Under step 2.2, continuing: by step 3.2 and the successor-menu form there are nonempty finite sets $F_n\subseteq T$ with every $x\in F_n$ having an $R$-successor in $F_{n+1}$; define $G_0:=F_0$ and $G_{n+1}:=\{u\in F_{n+1}:u=x^{⌢}a\text{ for some }x\in G_n\text{ and some }a\}$.

Under step 2.1, continuing: the sets $F_n$ of step 3.1 are nonempty finite subsets of $A$; extracting the last entry of each node uses only the defining data of the node, so no selection is made, and the successor condition verified in step 3.1 is exactly the menu condition of [F1].

Under step 4.1: by induction on $n$, each $G_n$ is a nonempty finite subset of $F_n$. The case $n=0$ is $G_0=F_0$. If $G_n$ is nonempty, choose $x\in G_n\subseteq F_n$; the menu property supplies an $R$-successor $u\in F_{n+1}$, and the definition of $G_{n+1}$ puts this $u$ in $G_{n+1}$. Finiteness follows from $G_{n+1}\subseteq F_{n+1}$. Moreover every $u\in G_{n+1}$ has a predecessor $x\in G_n$ by definition, and that predecessor is the canonical restriction of $u$ by [F2]; so the menus $G_n$ are coherent.

Under step 3.1 and step 4.2 we have produced a successor menu sequence for the arbitrary serial relation $R$ on the arbitrary nonempty set $A$; this is assertion 2 of the statement, so the tree form implies the successor-menu form.

Under step 4.1 and step 5.1, put $T^{\mathrm{\prime }}:=\{t\in T:t\subseteq s\text{ for some }s\in {\bigcup }_n{G}_n\}$, the downward closure in $T$ of the coherent menus. Then $T^{\mathrm{\prime }}$ is a subtree of $T$ by [F2]. Every level $T_m^{\mathrm{\prime }}$ is nonempty: for this fixed $m$, choose $x\in G_0$ and apply the successor half of coherence only $m$ times, by finite induction, to obtain $s\in G_m$ extending $x$. Since each step is an immediate extension, $\mathrm{dom}s=\mathrm{dom}x+m\ge m$, and $s\upharpoonright m\in T_m^{\mathrm{\prime }}$. This is one finite existence argument for the arbitrary level $m$, not a simultaneous choice of an infinite successor sequence.

Under step 6.1, each level $T_m^{\mathrm{\prime }}$ is finite. Indeed let $D:=\{\mathrm{dom}s:s\in G_0\}$, a finite set of natural numbers by [L2]. If $t\in T^{\mathrm{\prime }}$ has length $m$ and $t\subseteq s$ with $s\in G_k$, then iterating the canonical predecessor restriction from [F2] and [L1] gives $s\upharpoonright (\mathrm{dom}s-j)\in G_{k-j}$ for every $j\le k$. If $m\ge \mathrm{dom}s-k$, set $j:=\mathrm{dom}s-m\le k$ and $d:=\mathrm{dom}s-k\in D$; then $t=s\upharpoonright m\in G_{k-j}=G_{m-d}$. If instead $m<\mathrm{dom}s-k$, then $r:=s\upharpoonright (\mathrm{dom}s-k)\in G_0$ has length greater than $m$ and $t=r\upharpoonright m$. Hence $T_m^{\mathrm{\prime }}\subseteq \bigcup \{G_{m-d}:d\in D,d\le m\}\cup \{r\upharpoonright m:r\in G_0,\mathrm{dom}r>m\}$, a union of finitely many finite sets, which is finite.

Under step 6.1 and step 7.1 the subtree $T^{\mathrm{\prime }}$ of the arbitrary pruned tree $T$ has nonempty finite levels; this is assertion 1 of the statement, so the successor-menu form implies the tree form.

Steps 5.2 and 8.1 prove the two implications between assertions 1 and 2, so the two formulations of dependent multiple choice are equivalent over $\mathrm{Z}\mathrm{F}$.