Let CKDT be the assertion that for every countably infinite bipartite graph $G$, there exist a vertex covering $C$ of $G$ and a matching $M$ in $G$ such that $C$ consists of exactly one vertex from each edge in $M$. (This is a theorem of Podewski and Steffens [12].) Let $ATR_0$ be the subsystem of second-order arithmetic with arithmetical transfinite recursion and restricted induction. Let $RCA_0$ be the subsystem of second-order arithmetic with recursive comprehension and restricted induction. We show that CKDT is provable in $ART_0$. Combining this with a result of Aharoni, Magidor, and Shore [2], we see that CKDT is logically equivalent to the axioms of $ATR_0$, the equivalence being provable in $RCA_0$.
@article{1183744438,
author = {Simpson, Stephen G.},
title = {On the Strength of Konig's Duality Theorem for Countable Bipartite Graphs},
journal = {J. Symbolic Logic},
volume = {59},
number = {1},
year = {1994},
pages = { 113-123},
language = {en},
url = {http://dml.mathdoc.fr/item/1183744438}
}
Simpson, Stephen G. On the Strength of Konig's Duality Theorem for Countable Bipartite Graphs. J. Symbolic Logic, Tome 59 (1994) no. 1, pp. 113-123. http://gdmltest.u-ga.fr/item/1183744438/