Menger's theorem in \(\Pi^1_1 \mathrm {-CA}_0\) (Q412061)

The author studies the reverse mathematics of infinitary extensions of Menger's theorem from graph theory. The extension of finite Menger's theorem to countable graphs was proved in 1987 by \textit{R. Aharoni} [J. Comb. Theory, Ser. B 43, 303--313 (1987; Zbl 0631.05032)], but the extension to arbitrary graphs was only recently obtained by \textit{R. Aharoni} and \textit{E. Berger} [Invent. Math. 176, No. 1, 1--62 (2009; Zbl 1216.05092)]. The difficulty of the proof of the general result makes the theorem a natural candidate for reverse mathematics analysis. Previous work established only the lower bound that Menger's theorem for countable graphs implies the subsystem \(\text{ATR}_0\) of second-order arithmetic over the base system \(\text{RCA}_0\). This paper establishes an upper bound by showing that Menger's theorem for countable graphs is provable in the subsystem \(\Pi^1_1\text{-CA}_0\). The author poses the exact strength of Menger's theorem as an open question, but proves that a strengthened version, which the author calls extended Menger's theorem, is equivalent to \(\Pi^1_1\text{-CA}_0\) over \(\text{RCA}_0\). The proofs in \(\Pi^1_1\text{-CA}_0\) proceed via countable coded \(\beta\)-models and countable coded models of \(\Sigma^1_1\text{-DC}_0\).