Dependent multiple choice in finite-level tree form

Work in $\mathrm{Z}\mathrm{F}$ (The natural numbers $\mathbb{N}$ (von Neumann)); no choice principle is used or named in this definition beyond the one being introduced. Let $A$ be a set.

Nodes. A node over $A$ is a function $t:n\to A$ whose domain is a natural number $n$ (A function is a relation $f$ with $(a,b)\in f$ and $(a,c)\in f$ implying $b=c$; $f:A\to B$, the value $f(a)$, domain and codomain). Its length is $\mathrm{dom}t=n$ and its entries are the values $t(0),\dots ,t(n-1)$. The unique node of length $0$ is the empty sequence $\mathrm{\varnothing }$. For a node $t$ of length $n$, a natural $m\le n$ and $a\in A$ write

$t\upharpoonright m:=t\cap (m\times A),t^{⌢}a:=t\cup \{(n,a)\},$

the initial segment of length $m$ and the node of length $n+1$ obtained by appending $a$. A node $u$ is an immediate successor of $t$ when $u=t^{⌢}a$ for some $a\in A$, and a proper extension of $t$ when $t=u\upharpoonright \mathrm{dom}t$ and $\mathrm{dom}u>\mathrm{dom}t$.

Trees. A tree of height $\omega$ on $A$ is a set $T$ of nodes over $A$ such that $\mathrm{\varnothing }\in T$ and $t\upharpoonright m\in T$ whenever $t\in T$ and $m\le \mathrm{dom}t$. Its $n$-th level is

$T_n:=\{t\in T:\mathrm{dom}t=n\}\mathrm{.}$

The tree has nonempty levels when $T_n\mathrm{\ne }\mathrm{\varnothing }$ for every $n\in \mathbb{N}$, and finite levels when each $T_n$ is finite (The cardinality $\mid A\mid$ of a finite set). It is pruned, or serial, when every node has a proper extension in $T$. A subtree of $T$ is a subset of $T$ that is itself a tree of height $\omega$ on $A$.

The $R$-chain tree. Let $R\subseteq A\times A$ be a binary relation on $A$ and call $R$ serial on $A$ when every $x\in A$ has a successor: some $y\in A$ with $xRy$. The $R$-chain tree is

$T_R:=\{t:t\text{ a node over }A\text{ and }t(i)Rt(i+1)\text{ for every }i+1<\mathrm{dom}t\}\mathrm{.}$

It is a tree of height $\omega$ on $A$. For $A\mathrm{\ne }\mathrm{\varnothing }$ it is pruned exactly when $R$ is serial on $A$: a node of positive length has a proper extension precisely when its last entry $t(\mathrm{dom}t-1)$ has an $R$-successor, the empty node has the one-entry node $(a)$ as an extension for every $a\in A$, and the one-entry node $(a)$ has a proper extension exactly when $a$ has an $R$-successor. For $A=\mathrm{\varnothing }$ the equivalence fails: then $T_R=\{\mathrm{\varnothing }\}$, $R$ is vacuously serial on $A$, and the empty node has no proper extension. If $R$ is serial on $A$ and $A\mathrm{\ne }\mathrm{\varnothing }$, then every level of $T_R$ is nonempty, by iterating the successor condition.

Successor menus. Let $R$ again be a relation on $A$. A successor menu sequence for $R$ is a sequence $(F_n{)}_{n\in \mathbb{N}}$ of nonempty finite subsets $F_n\subseteq A$ such that

$\text{for every }n\text{ and every }x\in F_n\text{ there is }y\in F_{n+1}\text{ with }xRy\mathrm{.}$

It is coherent when in addition every $y\in F_{n+1}$ has a predecessor in $F_n$: some $x\in F_n$ with $xRy$. Downward closure makes the levels of any subtree of $T_R$ coherent in this predecessor sense, but it does not supply the forward-successor condition: a subtree with nonempty levels may have leaves. Its levels form a successor menu sequence only after restricting to nodes that continue to later levels, as carried out in the equivalence proof.

The two forms of DMC. Dependent multiple choice in tree form is the assertion

every pruned tree of height $\omega$ on every set $A$ whose levels are nonempty has a subtree with nonempty finite levels;

and dependent multiple choice in successor-menu form is the assertion

every serial relation on every nonempty set admits a successor menu sequence.

The menu form is the one recorded in Multiple choice and dependent multiple choice; the tree form is the one David Fremlin writes as ${\mathrm{D}\mathrm{M}\mathrm{C}}^{\mathrm{\prime }}$ and attributes to Blass (1979). The next theorem proves that the two assertions are equivalent over $\mathrm{Z}\mathrm{F}$.

• Pruning is a real condition. A subtree of a pruned tree need not be pruned: a node of a subtree with nonempty levels may have no extension inside the subtree. That is why the tree form above asks for the levels to be nonempty and finite but not for the subtree to be pruned, and why the proof of the equivalence has to prune the menus it obtains from the other form.

• Why the empty set is excluded from the menu form. A serial relation on $A=\mathrm{\varnothing }$ is serial vacuously, and there are no nonempty subsets of $A$ to serve as menus, so the menu form is stated for nonempty $A$. The tree form has no such exclusion: the tree consisting of the empty sequence alone has an empty level $1$ and is not a counterexample, because it is not pruned.

• The name DMC. The abbreviation is used for the principle over $\mathrm{Z}\mathrm{F}$ and is never asserted to be a theorem of $\mathrm{Z}\mathrm{F}$; the strictly weaker position of DMC among the choice principles is recorded separately on this page and is not part of this definition.