Cat Herding Game Played on Infinite Trees

We proceed by induction on $i$. The case $i=0$ is trivial, as a vertex itself is a binary tree minor of height $0$. Let $i>0$.

$(\Leftarrow )$ Suppose $v\in N$ is the root of a complete binary tree minor of height $i$. We must show $v\in V_i$. We proceed by observing the left and right children from $v$ in this minor, say $u_0,u_1$. These nodes are both a root of complete binary tree minor of height $i-1$. Nodes $u_0$ and $u_1$ are the good candidates to set the two existential quantified variables $y$ and $z$ in formula $\text{DBChildin}(X,x)$: indeed, they are both descendants of $v$ with edge-disjoint paths (by construction), and by induction, we have $u_0,u_1\in V_{i-1}$, giving us that $v\in V_i$.

$(\Rightarrow )$ Suppose that $v\in V_i$. There must be $u_0,u_1$ such that , $u_0,u_1\in V_{i-1}$, and there are edge-disjoint $v,u_0$ and $v,u_1$-paths. By induction, since $u_0,u_1\in V_{i-1}$, both $u_0,u_1$ must be roots of complete binary tree minors of height $i-1$. Combined with edge-disjoint $v,u_0$ and $v,u_1$-paths, $v$ must be the root of a binary tree minor of height $i$. $◀$

We now extend our semantics to capture what we loosely call here “transfinite iterations” of DBChildin, and that corresponds to the fix-point of a well-identified function in Lemma 12.

We proceed by transfinite induction on $\alpha$.

This is vacuously true for $\alpha =0$. If $\alpha +1$ is a successor ordinal, then $v\in V_{\alpha +1}$ implies there are edge-disjoint descendant paths to vertices in $V_{\alpha }$. But vertices in $V_{\alpha }$ must have descendant paths to vertices in $V_{\beta }$ for every . Composing these paths, we obtain edge-disjoint paths to every , as well as edge-disjoint paths to a pair of vertices in $V_{\alpha }$, thus giving every ordinal . Conversely, if $v$ has edge-disjoint paths to pairs of vertices in $V_{\beta }$ for all , then in particular $v$ has edge-disjoint paths to a pair of vertices in $V_{\alpha }$ since , and thus $v\in V_{\alpha +1}$.

If $\alpha$ is a limit ordinal, then $v\in V_{\beta +1}$ gives the paths to vertices in $V_{\beta }$, for any . Conversely, if $v$ has a pair of edge-disjoint paths to all , then it is in all $V_{\beta }$ by induction, and thus is in the intersection, so is in $V_{\alpha }$.$◀$

With the sets $V_{\alpha }$ and the preliminary properties expressed, we can consider the following function $f$ over the complete lattice $(2^N,\subseteq )$.

One can verify that the function $f$ is $\subseteq$-monotonic. By the Knaster-Tarski Theorem [18], the function $f$ has a greatest fix-point, that we write $\nu V.f(V)$⁴⁴4a classical notation, as for mu-calculus [13]..

We show that $V_{\alpha }$ is contained within all $V_{\beta }$ for $\beta \le \alpha$ by transfinite induction on $\alpha$.

If $\alpha$ is a limit ordinal or $0$, this is trivial. Otherwise, we only need to show that $V_{\alpha +1}\subseteq V_{\alpha }$, as this implies $V_{\alpha +1}\subseteq V_{\alpha }\subseteq V_{\beta }$ for all $\beta \le \alpha$, the same as all . As such, we must show that $f(V_{\alpha })\subseteq V_{\alpha }$. For $w\in f(V_{\alpha })$, we know that there are two edge-disjoint descendant paths to $u,v\in V_{\alpha }$. Each of these must have edge-disjoint paths to vertices in $V_{\beta }$ for all by Lemma 10. By combining these paths, we obtain that $w\in V_{\alpha }$ as was to be desired. $◀$

With no surprise, we obtain the following.

This a fairly standard proof, one may skip reading.

Since there is no set of all ordinals, we must bound the ordinals. However, each non-stabilizing iteration of $f$ removes at least one vertex, thus $V_{\alpha }$ need only be computed up and including to the order of $N$, making this a well-defined set.

We show $\nu V.f(V)\subseteq V_{\alpha }$ for all ordinals $\alpha$ by transfinite induction. Observe $\alpha =0$ is trivial. If $\alpha +1$ is a successor ordinal, then we observe that $w\in \nu V.f(V)$ implies $w$ has edge-disjoint paths to $u,v$ also in the fix-point. But then $u,v\in V_{\alpha }$ by induction. Thus $w\in V_{\alpha +1}$. Finally if is a limit ordinal, then $v\in \nu V.f(V)$ implies $v\in V_{\beta }$ for all by induction. Thus $v$ in the fix-point implies $v$ in the limit ordinal. Now, ${\bigcap }_{\alpha \le |N|}{V}_{\alpha }\supseteq \nu V.f(V)$ follows immediately from the first argument.

We now show ${\bigcap }_{\alpha \le |N|}{V}_{\alpha }\subseteq \nu V.f(V)$. We show $f({\bigcap }_{\alpha \le |N|}{V}_{\alpha })={\bigcap }_{\alpha \le |N|}{V}_{\alpha }$, so that ${\bigcap }_{\alpha \le |N|}{V}_{\alpha }$ is a fix-point, and by $\nu X$ being a greatest fix-point, we obtain the subset relation. If $v\in {\bigcap }_{\alpha \le |N|}{V}_{\alpha }$, then $v$ has edge-disjoint descendant path pairs to vertices in $V_{\alpha }$ for all $\alpha$ (using $v\in V_{\alpha +1}$). Thus $v\in f({\bigcap }_{\alpha \le |N|}{V}_{\alpha })$. Conversely, if $v\in f({\bigcap }_{\alpha \le |N|}{V}_{\alpha })$, then $v$ has edge-disjoint descendant paths to $x,y\in {\bigcap }_{\alpha \le |N|}{V}_{\alpha }$. Trivially $v\in V_0$. Next, $v\in V_{\alpha }$ implies $v\in V_{\alpha +1}$ since $v$ has paths to $x,y\in V_{\alpha }$. Finally, for limit ordinal $\alpha$, if $v\in V_{\beta }$ for all , then by definition $v\in V_{\alpha }$. Thus $v\in {\bigcap }_{\alpha \le |N|}{V}_{\alpha }$, and ${\bigcap }_{\alpha \le |N|}{V}_{\alpha }$ is a fix-point of $f$. $◀$ We will show that property $\nu V.f(V)=\mathrm{\varnothing }$ characterizes the herder-win trees, namely trees where herder has a strategy to capture the cat (whichever node the cat starts at). In service of this, we will provide herder strategies when a given rooted subtree has bounded ordinal $V_{\alpha }$ vertices. To do so, we will make frequent use of a herder strategy to force the cat off of a ray.

If the cat is not initially on $R$, then the herder disconnects $R$ from the cat. On a cat move to $x$ along this ray, the herder deletes the next vertex along the ray, isolating the cat to finitely many vertices of $R$. After finitely many moves, the herder may separate all of these vertices, and then make a passing move if necessary to force the cat off of the last one the cat has access to, and finally make a cut separating the cat from that vertex. Observe that as only the cat’s initial move may choose how many vertices of $R$ remain accessible after the herder’s cut, removing the cat’s access to this ray must be attainable within $\omega$ cuts – recall that $\omega$ is the least infinite ordinal greater than all the finite ordinals. $◀$ We further explain how herder captures the cat on subtrees of bounded $V_{\alpha }$.

Regardless of $\alpha$’s type, the herder begins by cutting $v_0$ from its parent if any, otherwise herder cuts an edge outgoing $v_0$. If the game does not terminate here, on the cat move to $v>v_0$, we split the argument on the type of ordinal $\alpha$.

If $\alpha =0$, the property trivially holds as it cannot be that $v\notin V_0(=V)$.

If $\alpha$ is a successor ordinal, then consider where descendants in $V_{\alpha -1}$ lie in the subtree below $v_0$. If ever two incomparable $u,u^{\prime }\in V_{\alpha -1}$, then their deepest common ancestor necessarily below or equal to $v_0$ would be in $V_{\alpha }$, a contradiction. Thus all elements of $V_{\alpha -1}$ are comparable, and thus lie on a single ray (or path). Apply Lemma 13 to force the cat off of all elements of $V_{\alpha -1}$, and apply the (transfinite) induction hypothesis on the resulting tree the cat is on, since all its vertices are outside $V_{\alpha -1}$.

If is a limit ordinal, then consider the set of $v_0$-rooted rays . If $ℛ$ contains at least two distinct rays, then there must be a first vertex at which they deviate, say $r$. By Lemma 10, $r$ must be in $V_{\alpha }$, a contradiction. Thus at most one ray may contain vertices in . We follow Lemma 13 to remove the cat’s access to this ray, and let $x\ge v_0$, be the new cat position. Now, every descendant vertex $w\ge x$ is outside some $V_{{\beta }_w}$, with . We show .

Suppose for contradiction ${sup}_{w\ge v}\{{\beta }_w\}=\alpha$. By Lemma 11, there must be infinitely many such that $V_{\beta }\ne \mathrm{\varnothing }$. Choose a representative $w\ge x$ with $w_{\beta }\in V_{\beta }$, so that $w_{\beta }$ is as close to the root as possible. Suppose have incomparable representatives $w_{\beta },w_{{\beta }^{\prime }}$. Then their least common ancestor should have been the candidate for $\beta$. Thus every representative is comparable, and they must lie on the same ray. But then we have another cat-accessible ray $r$ with $R\cap V_{\beta }\ne \mathrm{\varnothing }$ for all , a contradiction with the earlier herder-play. Thus $\{{\beta }_w|w\ge v\}$ is bounded, say by . We now use the transfinite induction where vertex $x\notin V_{\beta }$ can be used as the new root $v_0$ of Lemma 14.

Thus the ordinal has been reduced for the entire subtree and the cat’s location may again be interpreted as a root. $◀$

Note that these ray-themed arguments are reminiscent of the argument that the cat wins implies the existence of an infinite binary tree minor, but here the greatest fix-point characterization naturally leads us to reason about particular transfinite sets, yielding us a (transfinite) constructive herder strategy for capturing the cat.

We introduce the key formula $\text{ECW}(x)$ (for “Exists Cat Winning”) that characterizes the nodes the cat can start at and win by only downwards moves in tree. We will then make use the formula $\text{ECW}(x)$ (see formula $\text{CatWin}(x)$ in Equation 3) to describe the set of nodes the cat can start at and survive indefinitely.

We can now state our first main theorem.

We show more directions than necessary, as some provide different clarity on the argument.

• $\mathrm{■}$

  $(\text{<a href="\#S3.I4.i1" title="Item 1 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">1</span></a>})\Rightarrow (\text{<a href="\#S3.I4.i2" title="Item 2 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">2</span></a>})$. Argue by contrapositive as follows. Negating the logical statement of cat-win graphs, we obtain $T\vDash \forall x:\forall X:X(x)\Rightarrow \exists y:X(y)\wedge \neg \text{DBChildin}(X,y)$. This property in particular would hold for $X\mapsto \nu V.f(V)$ (the greatest fix-point of $f$) if non-empty, so that we must have $T\vDash \exists y:X(y)\wedge \neg \text{DBChildin}(X,y)$. The latter yields $\nu V.f(V)⊈f(\nu V.f(V))$, a contradiction for the fix-point. Therefore $\nu V.f(V)=\mathrm{\varnothing }$. By Lemma 12, ${\bigcap }_{\alpha \le |N|}{V}_{\alpha }=\mathrm{\varnothing }$, so that that for every node $v\in N$, we have $v\notin V_{{\alpha }_v}$ for some ${\alpha }_v$. Apply Lemma 14 with $v_0$ the root of $T$, to conclude that herder can capture the cat. Observe that Lemma 14 provides an explicit herder strategy for capturing the cat.

• $\mathrm{■}$

  $(\text{<a href="\#S3.I4.i2" title="Item 2 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">2</span></a>})\Rightarrow (\text{<a href="\#S3.I4.i3" title="Item 3 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">3</span></a>})$. We must construct some injective mapping $h$ from the infinite binary tree on ${\{0,1\}}^{\ast }$ to a subtree of $T$. Let $v\in N$ be a vertex such that $T,[x\mapsto v]\vDash \text{ECW}(x)$, and let $V\subseteq N$ be such that $T,[x\mapsto v,X\mapsto V]\vDash X(x)\wedge \exists y:X(y)\Rightarrow \text{DBChildin}(X,y)$. We define the mapping $h$ such that $h(s)\in V$, every $s\in {\{0,1\}}^{\ast }$.

  We proceed by induction over $s\in {\{0,1\}}^{\ast }$.

  • –

    $h(ϵ):=v\in V$ – the full binary tree minor we construct is rooted at $v$.

  • –

    Let node $s\in {\{0,1\}}^{\ast }$ be such that $h(s)$ has already been defined and therefore $h(s)\in V$. Then, we know that $T,[x\mapsto h(s),X\mapsto V]\vDash X(x)\wedge \exists y:X(y)\Rightarrow \text{DBChildin}(X,y)$, which in particular entails $T,[x\mapsto h(s),X\mapsto V]\vDash \text{DBChildin}(X,x)$. By definition of formula $\text{DBChildin}(X,x)$, node $h(s)$ has descendant nodes $u_0,u_1$ in $V$ on two different branches, that we naturally use to define $h(s0)$ and $h(s1)$ respectively.

  Note that by construction $h$ is injective, as $h(s0)$ and $h(s1)$ are disjoint and that we target vertices deeper and deeper in the tree. Say a node is $h$-hit if it is in the image of $h$. The complete infinite binary tree minor of $T$ is obtained by contracting all edges with at most one $h$-hit node.

• $\mathrm{■}$

  $(\text{<a href="\#S3.I4.i3" title="Item 3 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">3</span></a>})\Rightarrow (\text{<a href="\#S3.I4.i4" title="Item 4 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">4</span></a>})$. Immediate from the uncountability of the set of all infinite binary sequences, corresponding to rays.

• $\mathrm{■}$

  $(\text{<a href="\#S3.I4.i4" title="Item 4 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">4</span></a>})\Rightarrow (\text{<a href="\#S3.I4.i1" title="Item 1 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">1</span></a>})$ by contrapositive. We must show that if the herder wins, then the rays $ℛ$ are countable. Observe the $i$th cut may remove the cat from accessing infinitely much of a given ray $R$. Let ${ℛ}_i$ to be the set of rays which the cat could access infinitely much of before the $i$th cut, but only finitely much after the $i$th cut. We argue ${ℛ}_i$ is countable and ${\bigcup }_i{ℛ}_i=ℛ$. By contradiction, if there exists an $i$th cut that makes ${ℛ}_i$ uncountable, then the cat made a bad move. Suppose the cat instead went to just on the other side of the herder cut. Then we get uncountably many rays available now, but the herder’s cut may change. If iterating this process to get successively better cat moves happens to move the cat’s choices upwards (towards the root), it must terminate, and ${ℛ}_i$ is countable. If downwards (away from the root), get uncountably many rays with same prefix, for any prefix length. In the limit, obtain ray $\pi$. Then enumerate all rays starting with $\pi$, then $1$ ray deviating at depth $1$, then $1,2,1,2,3,\mathrm{\dots }$. A given ray $R$ has $R=\pi$ or $R$ deviates from $\pi$ at depth $d$. But depth $d$ deviations are countable, and our enumeration of $ℛ$ checks depth $d$ infinitely many times, so $R$ is counted. Thus $ℛ$ is countable, as was to be shown. Alternately, the cat can make a strategy that never lets ${ℛ}_i$ be uncountable, so that ${ℛ}_i$ is always countable, and there are finitely many of them. Thus ${\bigcup }_i{ℛ}_i$ is countable. But $ℛ={\bigcup }_i{ℛ}_i$ since clearly ${ℛ}_i\subseteq ℛ$, and if $R\in ℛ$, then since the herder won after $i$ steps, the cat must have access to at most one vertex of $R$, and so the cat must have had access to infinitely many vertices of $R$ removed at some point, say $i$. Thus $R\in {ℛ}_i$ for some $i$. We have thus counted the set of all rays.

• $\mathrm{■}$

  $(\text{<a href="\#S3.I4.i2" title="Item 2 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">2</span></a>})\Rightarrow (\text{<a href="\#S3.I4.i1" title="Item 1 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">1</span></a>})$. We include this direction to make the cat’s winning strategy explicit. Since $T\vDash \exists x:\text{ECW}(x)$, we have a node $v_0\in N$ and a set $V\subseteq N$ such that $T,[x\mapsto v_0,X\mapsto V]\vDash X(x)\wedge \exists y:X(y)\Rightarrow \text{DBChildin}(X,y)$. Thus $V\ne \mathrm{\varnothing }$. The cat’s strategy will be to always play to a vertex $v\in V$ and has all herder cuts incomparable or ancestors of the cat’s current position. This is possible, since on any herder cut when the cat is at $v$ and $T,[x\mapsto v,X\mapsto V]\vDash \text{DBChildin}(X,x)$. By expanding formula $\text{DBChildin}(X,x)$, we get , so that that there are $u_0,u_1$ with $T,[x\mapsto v,y\mapsto u_0,z\mapsto u_1,X\mapsto V]\vDash \text{DB}(x,y,z)$. The latter implies that no single edge cut from the herder could remove the cat’s path to both $u_0$ and $u_1$, and the herder only gets one cut as $u_0,u_1>x$, and all previous cuts were ancestors or incomparable. Thus the cat can move to $u_0$ or $u_1$, and $u_0,u_1\in V$ are both promised, giving the invariant the cat seeks. Note this also corresponds to playing on a root of a complete infinite binary tree minor, so that $(\text{<a href="\#S3.I4.i3" title="Item 3 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">3</span></a>})\Rightarrow (\text{<a href="\#S3.I4.i1" title="Item 1 ‣ Theorem 15. ‣ Proof. ‣ 3.2 MSO for Cat Herding game on infinite tree arenas ‣ 3 Cat Herding played on Infinite Trees ‣ Cat Herding Game Played on Infinite Trees" class="ltx\_ref ltx\_font\_italic"><span class="ltx\_text ltx\_ref\_tag">1</span></a>})$ could have been shown instead similarly.

It follows that conditions (1)-(4) are equivalent. $◀$

As a final matter of logical completeness, we provide our second main theorem (Theorem 16), by considering the following formula that characteres all nodes that the cat can start at and still win.

It is clear that the formula $\text{ECW}(x)\Rightarrow \text{CatWin}(x)$ always holds, but the reciprocal does not. To see this, consider a complete binary tree where the topmost edges are subdivided once; formally, the set of nodes is $(0+00+1+11){(0\cup 1)}^{\ast }$. The cat starting at node $0$ can win by moving to vertex $00$ or $11$ (depending on herder’s first cut), and because either if these two nodes satisfies $\text{ECW}(x)$, the cat can survive indefintely. However, the node $0$ the cat started from itself does not satisfy $\text{ECW}(x)$: indeed, any two branches from $0$ both cross edge $(0,00)$ and therefore cannot be disjoint as required by Equation 2 for $\text{ECW}(x)$.

In this proof, we may abuse notation and conflate $\text{ECW},\text{CatWin}\subseteq N$ as a set of nodes with the predicate.

($\Leftarrow$) By contrapositive, suppose $T,[x\mapsto v_0]\vDash \neg \text{CatWin}(x)$. Then $T,[x\mapsto v_0]\vDash \forall y\forall z:\text{DB}(x,y,z)\Rightarrow \left(\neg \text{ECW}(y)\vee \neg \text{ECW}(z)\right)$. Since by assumption $v_0\notin \text{CatWin}$, and because $\text{ECW}\subseteq \text{CatWin}$, $v_0\notin \text{ECW}$ so that all vertices from ECW below $v_0$ are on a same branch. The herder’s strategy is to cut this branch from $v_0$. The resulting tree fails condition 2 of Theorem 15, and so the herder wins now.

($\Rightarrow$) Suppose $v_0\in \text{CatWin}$. Then on the cat starting at $v_0$, after any cut, the cat may move to a vertex satisfying ECW (using edge-disjointness of $x,u$ and $x,v$-paths). Then the strategy of (2 implies 1) in Theorem 15 gives the cat a way to win once in ECW. $◀$