Proof of the Main Theorem

The purpose of this section is to prove our main result:

Theorem 1   The König duality theorem for countable bipartite graphs (i.e. CKDT) is provable in $\hbox{\em ATR}_0$.

In order to prove Theorem 1, the following notions will be useful. Let G=(X,Y,E) be a bipartite graph. For $y\in Y$, the neighborhood of y in G is

$$N_G(y)=\{x\in X:\{x,y\}\in E\}\,.$$

For $A\subseteq X$, the demand of A with respect to G is

$$D_G(A)=\{y\in Y:N_G(y)\subseteq A\}\,.$$

For $A\subseteq X$ and $B\subseteq Y$, a matching of A into B is a matching M such that $X\cap(\bigcup M)=A$ and $Y\cap(\bigcup M)\subseteq B$. In this case we write

$$M:A\to B$$

and, for $x\in A$, M(x)= the unique y such that $\{x,y\}\in M$. Thus

$$M=\{\{x,M(x)\}:x\in A\}\,.$$

If M is any matching in Gand if v and w are vertices of G, an M-alternating path from v to wis a sequence of vertices v=v₀, v₁, ..., v_n=w such that $\{v_i,v_{i+1}\}\in E\hbox{ for all }i<n$, $\{v_i,v_{i+1}\}\in M\hbox{ for all odd }i<n$, and $\{v_i,v_{i+1}\}\notin M\hbox{ for all even }i<n$.

We now begin the proof of Theorem 1. We reason in $\mathsf{ATR}_0$. Let G=(X,Y,E) be a countable bipartite graph. We shall prove in $\mathsf{ATR}_0$ that a König covering of G exists.

By Lemma 1, there exists a countable coded $\omega$-model ${\mathcal M}$of $\Sigma^1_1$- $\mathsf{AC}_0$ such that $G\in{\mathcal M}$. Fix such an ${\mathcal M}$. Let A^* be the union of all sets $A\subseteq X$ such that $A\in{\mathcal M}$ and in ${\mathcal M}$ there is a matching $F:A\to D_G(A)$. Note that A^* is definable over ${\mathcal M}$. Hence A^* exists by arithmetical comprehension, using a code of ${\mathcal M}$ as a parameter.

Lemma 2   There exists a matching $F^*:A^*\to D_G(A^*)$.

Proof. By arithmetical comprehension using a code of ${\mathcal M}$ as a parameter, we can find an enumeration $\left\langle(A_n,F_n):n\in\mathbb{N}\right\rangle$ of all pairs $(A,F)\in{\mathcal M}$ such that F is a matching of A into D_G(A). Then $A^*=\bigcup\{A_n:n\in\mathbb{N}\}$. For $x\in A^*$ define F^*(x)=F_n(x) where n= the least n such that $x\in A_n$. To see that F^* is one-to-one, suppose F^*(x₁)=F^*(x₂)=y. For i=1,2 put n_i= the least n such that $x_i\in A_n$. Then F_n1(x₁)=F_n2(x₂)=y. Hence $y\in D_G(A_{n_1})\cap D_G(A_{n_2})$. Hence $x_1,x_2\in A_{n_1}\cap A_{n_2}$. It follows that n₁=n₂. Hence x₁=x₂. Thus F^* is a matching, and clearly $F^*:A^*\to D_G(A^*)$. This proves the lemma.

Put X^*=X-A^* and Y^*=Y-D_G(A^*). We shall need to consider certain subgraphs of G of the form

$$G'=G-\{x_0,\dots,x_{n-1},y_0,\dots,y_{n-1}\}$$

where x₀, ..., $x_{n-1}\in X^*$and y₀, ..., $y_{n-1}\in Y^*$. For any such graph G' we shall use the notation G'=(X',Y',E') where $X'=X-\{x_0,\dots,x_{n-1}\}$, $Y'=Y-\{y_0,\dots,y_{n-1}\}$, and $E'=E\cap\{\{x,y\}:x\in X',y\in Y'\}$. Note that for any such graph G' we have $G'\in{\mathcal M}$.

Let G' be a subgraph of G as above. We say that G' is good if there is no set $A\subseteq X'$ such that $A\in{\mathcal M}$and in ${\mathcal M}$ there is a matching $F:A\to D_{G'}(A)$ such that

$$\left(D_{G'}(A)-\bigcup F\right)\cap Y^*\,\neq\,\emptyset\,.$$

Lemma 3   G is good.

Proof. Let $A\subseteq X$ be such that $A\in{\mathcal M}$and in ${\mathcal M}$ there is a matching $F:A\to D_G(A)$. Then $A\subseteq A^*$. Hence $D_G(A)\subseteq D_G(A^*)$. Hence by the definition of Y^* we have $D_G(A)\cap Y^*=\emptyset$. This shows that G is good.

Lemma 4   Suppose G' is good. Suppose $x\in X'\cap X^*$ and $y\in Y'\cap Y^*$are such that $G'-\{x,y\}$ is not good. Then there exists $A'\subseteq X'$ such that $x\in A'$ and $A'\in{\mathcal M}$ and in ${\mathcal M}$ there is a matching $F':A'\to D_{G'}(A')$ such that $y\notin\bigcup F'$.

Proof. Since $G'-\{x,y\}$ is not good, we can find a set $A\subseteq X'-\{x\}$, $A\in{\mathcal M}$, a matching $F:A\to D_{G'-\{x,y\}}(A)$, $F\in{\mathcal M}$, and a vertex $y^*\in (D_{G'-\{x,y\}}(A)-\bigcup F)\cap Y^*$.

We claim that there exists an F-alternating path in G'from y^* to x. To see this, let S be the set of all $x'\in X'-\{x\}$ such that there exists an F-alternating path in $G'-\{x,y\}$ from y^* to x', and let T be the set of all $y'\in Y'-\{y\}$ such that there exists an F-alternating path in $G'-\{x,y\}$ from y^* to y'. For any $x'\in S$ we clearly have $F(x')\in T$. Thus $F_S=\{\{x',F(x')\}:x'\in S\}$ is a matching of S into T. Note also that S, T, and F_S belong to ${\mathcal M}$. Moreover, for any $y'\in T$ we clearly have $N_{G'-\{x,y\}}(y')\subseteq S$. Thus $T\subseteq D_{G'-\{x,y\}}(S)$. However, since G' is good and $y^*\in (T-\bigcup F_S)\cap Y^*$, we cannot have $T\subseteq D_{G'}(S)$. Hence there must exist $y'\in T$ such that $\{x,y'\}\in E'$. Let y^*=y'₀, x'₀, y'₁, x'₁, ...,y'_n=y'be an F-alternating path in $G'-\{x,y\}$from y^* to y'. Then y^*=y'₀, x'₀, y'₁, x'₁, ..., y'_n, x'_n=xis an F-alternating path in G' from y^* to x. This proves the claim.

Put $A'=A\cup\{x\}$. Then obviously $D_{G'-\{x,y\}}(A)\subseteq D_{G'}(A')$. Using our F-alternating path y^*=y'₀, x'₀, y'₁, x'₁, ..., y'_n, x'_n=xas above, put

$$F'=\left(F-\{\{x'_i,y'_{i+1}\}:i<n\}\right)\cup\{\{x'_i,y'_i\}:i\leq n\}\,.$$

Since F is a matching of A into $D_{G'-\{x,y\}}(A)$, and since $x,y^*\notin\bigcup F$ and $y^*\in D_{G'-\{x,y\}}(A)$, it follows that F' is a matching of A' into $D_{G'-\{x,y\}}(A)$. Therefore, F' is a matching of A' into D_G'(A'). It is also clear that $x\in A'$, $A'\in{\mathcal M}$, $F'\in{\mathcal M}$, and $y\notin\bigcup F'$. This completes the proof of Lemma 4.

Lemma 5   Suppose that G' is good. Then for all $y\in Y'\cap Y^*$there exists $x\in X'\cap X^*$ such that $\{x,y\}\in E'$ and $G'-\{x,y\}$ is good.

Proof. Fix $y\in Y'\cap Y^*$and assume for a contradiction that there is no $x\in X'\cap X^*$ such that $\{x,y\}\in E'$ and $G'-\{x,y\}$ is good.

We claim that for all $x\in N_{G'}(y)$ there exists $(A',F')\in{\mathcal M}$ such that $x\in A'$, $A'\subseteq X'$, F' is a matching of A' into D_G'(A'), and $y\notin\bigcup F'$. We prove this claim by considering two cases, $x\in A^*$ and $x\notin A^*$. If $x\notin A^*$, then $x\in X'\cap X^*$and by assumption $G'-\{x,y\}$ is not good, so the claim follows by Lemma 4. If $x\in A^*$, then by the definition of A^*we can find a set $A\subseteq X$, $A\in{\mathcal M}$, $x\in A$, and a matching $F:A\to D_G(A)$, $F\in{\mathcal M}$. Then $A\subseteq A^*\subseteq X'$and $D_G(A)\subseteq D_G(A^*)\subseteq Y'$, hence $D_G(A)\subseteq D_{G'}(A)$. Moreover $y\in Y^*=Y-D_G(A^*)$, hence $y\notin D_G(A)$, hence $y\notin\bigcup F$. Thus in this case our claim holds with (A',F')=(A,F). This completes the proof of the claim.

Working within ${\mathcal M}$, let $\left\langle x'_n:n\in\mathbb{N}\right\rangle$be an enumeration of the vertices in N_G'(y). The above claim implies that for all $n\in\mathbb{N}$there exists $(A',F')\in{\mathcal M}$ such that $x'_n\in A'$, $A'\subseteq X'$, F' is a matching of A' into D_G'(A'), and $y\notin\bigcup F'$. Applying the $\Sigma^1_1$ Countable Choice Scheme within ${\mathcal M}$, we obtain a sequence $\left\langle(A'_n,F'_n):n\in\mathbb{N}\right\rangle\in{\mathcal M}$such that for all $n\in\mathbb{N}$ we have $x'_n\in A'_n$, $A'_n\subseteq X'$, F'_n is a matching of A'_n into D_G'(A'_n), and $y\notin\bigcup F'_n$.

Put $A=\bigcup\{A'_n:n\in\mathbb{N}\}$. Then $N_{G'}(y)=\{x'_n:n\in\mathbb{N}\}\subseteq A$, i.e. $y\in D_{G'}(A)$. Still working within ${\mathcal M}$, define F(x) for all $x\in A$ by F(x)=F'_n(x)where n= the least n such that $x\in A'_n$. To see that F is one-to-one, suppose F(x')=F(x'')=y'. Let n'= the least n such that $x'\in A'_n$, and let n''= the least n such that $x''\in A'_n$. Then F'_n'(x')=F'_n''(x'')=y'. Hence $y'\in D_{G'}(A'_{n'})\cap D_{G'}(A'_{n''})$. Hence $x',x''\in A'_{n'}\cap A'_{n''}$. It follows that n'=n''. Hence x'=x''. Thus F is a matching. Clearly $F:A\to D_{G'}(A)$and we also clearly have $A\in{\mathcal M}$, $F\in{\mathcal M}$, and $y\in (D_{G'}(A)-\bigcup F)\cap Y^*$. This contradicts the assumption that G' is good. The proof of Lemma 5 is complete.

We are now ready to finish the proof of Theorem 1. Still reasoning within $\mathsf{ATR}_0$, fix a one-to-one enumeration y₀, y₁, ..., y_n, ... of all the vertices in Y^*. The idea of this part of the proof is to apply Lemma 5 repeatedly to obtain a sequence of vertices x₀, x₁, ..., x_n, ...in X^*so that

$$H=\{\{x_0,y_0\},\{x_1,y_1\},\dots,\{x_n,y_n\},\dots\}$$

will be a matching. To begin, since G is good and $y_0\in Y^*$, we can apply Lemma 5 with G'=G and y=y₀ to obtain $x_0\in X^*$ such that $\{x_0,y_0\}\in E$ and $G-\{x_0,y_0\}$ is good. Next, since $G-\{x_0,y_0\}$ is good and $y_1\in Y^*-\{y_0\}$, we can apply Lemma 5 with $G'=G-\{x_0,y_0\}$ and y=y₁to obtain $x_1\in X^*-\{x_0\}$ such that $\{x_1,y_1\}\in E$and $G-\{x_0,y_0,x_1,y_1\}$ is good. At stage n of the construction, we assume inductively that $G-\{x_0,y_0,\dots,x_{n-1},y_{n-1}\}$ is good. Since $y_n\in Y^*-\{y_0,\dots,y_{n-1}\}$, we can apply Lemma 5 with $G'=G-\{x_0,y_0,\dots,x_{n-1},y_{n-1}\}$ and y=y_nto obtain $x_n\in X^*-\{x_0,\dots,x_{n-1}\}$ such that $\{x_n,y_n\}\in E$ and $G-\{x_0,y_0,\dots,x_n,y_n\}$ is good. The inductive construction of the sequence x₀, x₁, ..., x_n, ... is definable over ${\mathcal M}$. Thus H exists by arithmetical comprehension, using a code of ${\mathcal M}$ as a parameter.

Clearly H is a matching, $X\cap(\bigcup H)\subseteq X^*$, and $Y\cap(\bigcup H)=Y^*$. In addition, Lemma 2 provides a matching $F^*:(X-X^*)\to(Y-Y^*)$. Thus $F^*\cup H$ is again a matching. Since D_G(X-X^*)=Y-Y^*, it follows that $((X-X^*)\cup Y^*,F^*\cup H)$ is a König covering of G. This completes the proof of Theorem 1.