König 边染色定理的逻辑强度

König 边染色定理说，最大度为 $n$ 的二部图具有不超过 $n$ 种颜色的边染色。我们探讨该定理的可计算性理论与逆数学方面。度以 $n$ 为界的 computable 二部图具有带 $n+1$ 种颜色的 computable 边染色，但存在带 $n$ 种颜色的边染色这一定理在 RCAo 上等价于 WKLo。这给出了 Hirst 定理的附加证明：在 RCAo 上 WKLo 等价于每个可数二部 $n$-正则图是 $n$ 个完全匹配的并这一原理。我们描述与 Vizing 边染色定理和 Birkhoff 定理的可数形式相关的开放问题。