Partial partitions, unfriendliness at a vertex, and the partitioning game with an ordinal clock

Setting and notation. Throughout, $V$ is an arbitrary type (the vertex set) living in a universe $u$; $V$ may be empty, finite or infinite. $G$ is a simple graph on $V$, i.e. a binary adjacency relation $v \sim_G w$ on $V$ that is symmetric and irreflexive (no loops, no multiple edges, and no further restriction: a vertex may have infinitely many neighbours). $N_G(v) = \{\, w \in V : v \sim_G w \,\}$ is the set of neighbours of $v$. A partial 2-colouring is any function $f : V \to \{\bot, \mathsf T, \mathsf F\}$, where $\bot$ means "no colour assigned" and $\mathsf T, \mathsf F$ are the two Boolean colours; for a Boolean $b$, $\bar b$ denotes its negation ($\bar{\mathsf T} = \mathsf F$, $\bar{\mathsf F} = \mathsf T$). $|X|$ denotes the cardinality of $X$ as a cardinal number (in universe $u$), so it may be infinite, and $\le$ between cardinalities means existence of an injection. Ordinals $\alpha, \beta, r$ range over the ordinals of a second universe $v$, independent of $u$; $\beta < \alpha$ is the usual strict well-ordering of ordinals.

Definition NeighColored (written $N^{f}_{b}(v)$). For any type $B$, any function $f : V \to B$, any vertex $v \in V$ and any value $b \in B$, $N^f_b(v)$ is the type (in universe $u$) whose elements are the members of the set

$$N^f_b(v) \;=\; N_G(v) \cap f^{-1}(\{b\}) \;=\; \{\, w \in V : v \sim_G w \ \text{ and } \ f(w) = b \,\},$$

i.e. the neighbours of $v$ whose $f$-value is exactly $b$. (Below it is only ever used with $B = \{\bot,\mathsf T,\mathsf F\}$ and $b \in \{\mathsf T,\mathsf F\}$.)

Definition UnfriendlyAt (written $\mathrm{Unf}(G, f, v)$). For a partial 2-colouring $f : V \to \{\bot,\mathsf T,\mathsf F\}$ and a vertex $v \in V$:

$$\mathrm{Unf}(G,f,v) \iff \exists\, b \in \{\mathsf T,\mathsf F\}\ \text{ such that }\ f(v) = b \ \text{ and }\ \bigl|N^f_{b}(v)\bigr| \;\le\; \bigl|N^f_{\bar b}(v)\bigr| .$$

In words: $v$ is actually coloured (so $f(v) \ne \bot$; the witness $b$ is forced to be the colour of $v$), and the number of neighbours of $v$ carrying the same colour as $v$ is at most, as cardinals, the number of neighbours carrying the opposite colour. Neighbours with $f(w) = \bot$ are counted on neither side. Edge cases that the definition literally includes: a coloured vertex with no neighbours satisfies it ($0 \le 0$); if both sides are infinite of the same cardinality the inequality holds; if the same-colour side is infinite and the opposite side finite it fails; an uncoloured vertex ($f(v) = \bot$) is never unfriendly.

Definition emptyPartition (written $f_\emptyset$). For a type $V$ (universe $u$), $f_\emptyset : V \to \{\bot,\mathsf T,\mathsf F\}$ is the constant function $f_\emptyset(v) = \bot$ for all $v$ (no vertex coloured).

Definition HasFiniteDomain (written $\mathrm{FinDom}(f)$). For $f : V \to \{\bot,\mathsf T,\mathsf F\}$,

$$\mathrm{FinDom}(f) \iff \{\, v \in V : f(v) \ne \bot \,\} \ \text{ is a finite set},$$

i.e. there are $n \in \mathbb N$ and a bijection between this set and $\{0,\dots,n-1\}$; $n = 0$ is allowed, so $f_\emptyset$ has finite domain.

Definition Extends (written $f \preceq g$). For $f, g : V \to \{\bot,\mathsf T,\mathsf F\}$,

$$f \preceq g \iff \forall v \in V,\ \forall b \in \{\mathsf T,\mathsf F\}:\quad f(v) = b \;\Rightarrow\; g(v) = b .$$

Every colour already assigned by $f$ is kept unchanged by $g$. Nothing is required at vertices with $f(v) = \bot$: $g$ may colour them or leave them uncoloured. In particular $f \preceq f$, and $f_\emptyset \preceq g$ for every $g$.

Definition IsLegalResponse (written $L(G, f, g, v)$). For $f, g : V \to \{\bot,\mathsf T,\mathsf F\}$ and $v \in V$,

$$L(G,f,g,v) \iff (f \preceq g)\ \wedge\ \mathrm{FinDom}(g)\ \wedge\ \mathrm{Unf}(G, g, v).$$

No hypothesis is placed on $f$ itself (although $f \preceq g$ together with $\mathrm{FinDom}(g)$ forces the coloured set of $f$ to be finite as well). $g$ is not required to differ from $f$; $g$ is required to be unfriendly only at the single vertex $v$ and nothing is asserted about other vertices; $g$ may colour any finite number of further vertices anywhere in $V$.

Definition PartitionerWins (written $W(G, f, \alpha)$). For a partial 2-colouring $f : V \to \{\bot,\mathsf T,\mathsf F\}$ and an ordinal $\alpha$ (universe $v$), $W(G,f,\alpha)$ is defined by well-founded recursion on $\alpha$ (the recursive call is at an ordinal $\beta < \alpha$):

$$W(G,f,\alpha) \iff \forall v \in V,\ \ \forall \beta < \alpha,\ \ \exists\, g : V \to \{\bot,\mathsf T,\mathsf F\}:\quad L(G,f,g,v)\ \wedge\ W(G,g,\beta).$$

In words: for every vertex $v$ (any vertex at all, coloured or not under $f$; the same vertex may be chosen again at later stages) and for every ordinal $\beta$ strictly smaller than $\alpha$ (all such $\beta$, not only an immediate predecessor; at a limit $\alpha$ this is every $\beta < \alpha$), there exists a $g$ that extends $f$, colours only finitely many vertices, and is unfriendly at $v$ (the choice of $g$ may depend on both $v$ and $\beta$), and the same property holds again from the pair $(g, \beta)$. Unfolding the recursion, this is a sequence of alternations: an opponent picks $(v_0, \beta_0)$ with $\beta_0 < \alpha$, the Partitioner answers $g_0$ with $L(G,f,g_0,v_0)$; the opponent picks $(v_1,\beta_1)$ with $\beta_1 < \beta_0$, the Partitioner answers $g_1$ with $L(G,g_0,g_1,v_1)$; and so on; since the ordinals $\beta_0 > \beta_1 > \cdots$ strictly decrease, every such run is finite. Consequences of the literal definition: $W(G,f,0)$ holds for every $G$ and every $f$ (there is no $\beta < 0$), including $f$ with infinitely many coloured vertices; if $V$ is empty then $W(G,f,\alpha)$ holds for every $\alpha$; if $\alpha > 0$, $V$ is nonempty and $f$ has infinitely many coloured vertices, then $W(G,f,\alpha)$ fails (no finite-domain $g$ extends $f$).