The logical strength of K\"onig's edge coloring theorem

Abstract

K\"onig's edge coloring theorem says that a bipartite graph with maximal degree $n$ has an edge coloring with no more than $n$ colors. We explore the computability theory and Reverse Mathematics aspects of this theorem. Computable bipartite graphs with degree bounded by $n$ have computable edge colorings with $n+1$ colors, but the theorem that there is an edge coloring with $n$ colors is equivalent to WKLo over RCAo. This gives an additional proof of a theorem of Hirst: WKLo is equivalent over RCAo to the principle that every countable bipartite $n$-regular graph is the union of $n$ complete matchings. We describe open questions related to Vizing's edge coloring theorem and a countable form of Birkhoff's theorem.