Introduction

A bipartite graph is an ordered triple G=(X,Y,E)such that X and Y are sets, $X\cap Y=\emptyset$, and $E\subseteq\{\{x,y\}:x\in X,y\in Y\}$. The vertices of G are the elements of $X\cup Y$. The edges of G are the elements of E.

A covering of G is a set $C\subseteq X\cup Y$ such that every edge of G has a vertex in C, i.e. we have $C\cap e\neq\emptyset$ for all $e\in E$.

A matching in G is a pairwise disjoint set $M\subseteq E$. Here pairwise disjointness means that no two edges in M have a common vertex, i.e. we have $e_1\cap e_2=\emptyset$ for all $e_1,e_2\in M$such that $e_1\neq e_2$.

For any set S we use |S| to denote the cardinality of S, i.e. the number of elements in S. If G is any bipartite graph and C is any covering of Gand M is any matching in G, then clearly $\vert C\vert\geq\vert M\vert$. The König duality theorem [7] asserts that, for any finite bipartite graph G, there exist a covering C of Gand a matching M in G such that |C|=|M|. In other words,

$$\min\{\vert C\vert:C\hbox{ is a covering of }G\}= \max\{\vert M\vert:M\hbox{ is a matching in }G\}\,.$$

Definition 1.1   For any bipartite graph G, a König covering of G is an ordered pair (C,M) such that C is a covering of G, M is a matching in G, and C consists of exactly one vertex from each edge of M. (The last condition means that $C\subseteq\bigcup M$ and $\vert C\cap e\vert=1$ for each $e\in M$.)

Clearly if (C,M) is a König covering of G then |C|=|M|. König [7] showed that every finite bipartite graph has a König covering. From this the König duality theorem follows immediately.

Podewski, Steffens and Aharoni extended the König duality theorem to infinite bipartite graphs. In order to make such extensions meaningful, they considered König coverings. Podewski and Steffens [12] showed that every countably infinite bipartite graph has a König covering. Aharoni [1] showed that every uncountable bipartite graph has a König covering. We refer to the Podewski-Steffens theorem (respectively Aharoni's theorem) as the König duality theorem for countable (respectively uncountable) bipartite graphs.

Aharoni, Magidor and Shore [2] considered the following logical or foundational question: Which set existence axioms are needed to prove the König duality theorem for countable bipartite graphs? Aharoni, Magidor and Shore obtained a partial answer to this question, but they did not answer it completely. The purpose of this paper is to finish the work which was begun by Aharoni, Magidor and Shore.

The general question of which set existence axioms are needed to prove specific mathematical theorems is of basic importance for the foundations of mathematics. This general question has been studied fruitfully in the context of subsystems of second order arithmetic. For this purpose, five of the most important subsystems of second order arithmetic are $\mathsf{RCA}_0$, $\mathsf{WKL}_0$, $\mathsf{ACA}_0$, $\mathsf{ATR}_0$, and $\Pi^1_1$- $\mathsf{CA}_0$. It is known that these five systems are of strictly increasing strength as regards their ability to prove mathematical theorems. Moreover, for many particular mathematical theorems, it turns out that one can determine the weakest natural subsystem of second order arithmetic in which the given mathematical theorem is provable. Such results are established by showing that the given mathematical theorem is logically equivalent to the axioms of the specified subsystem of second order arithmetic, the equivalence being proved in a weaker system. Consider for example the Bolzano-Weierstrass theorem: every bounded sequence of real numbers has a convergent subsequence. It is known that the weakest subsystem of second order arithmetic in which the Bolzano-Weierstrass theorem is provable is $\mathsf{ACA}_0$. This is established by showing that the Bolzano-Weierstrass theorem is logically equivalent to the axioms of $\mathsf{ACA}_0$, the equivalence being proved in the weaker system $\mathsf{RCA}_0$.

For a survey of subsystems of second order arithmetic and their role in foundational studies, see my article [16]. A fuller treatment will appear in [17]. For additional results and open problems concerning logical and foundational aspects of combinatorics, see the articles in Logic and Combinatorics [8], especially [3].

Aharoni, Magidor and Shore [2] made a major contribution to the foundational program of [16]. They obtained two important results. First, the König duality theorem for countable bipartite graphs (i.e. CKDT) is provable in $\Pi^1_1$- $\mathsf{CA}_0$. Second, CKDT logically implies the axioms of $\mathsf{ATR}_0$, this implication being provable in the weak system $\mathsf{RCA}_0$. (Aharoni, Magidor and Shore also obtained results concerning logical aspects of some other infinitistic variants of the König duality theorem.)

The main result of the present paper is that the König duality theorem for countable bipartite graphs is provable in $\mathsf{ATR}_0$. This is established in Section 3 below. Combining this with the results of Aharoni, Magidor and Shore, we see that CKDT is logically equivalent to the axioms of $\mathsf{ATR}_0$, the equivalence being provable in $\mathsf{RCA}_0$. Thus $\mathsf{ATR}_0$ is the weakest natural subsystem of second order arithmetic in which CKDT is provable.