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

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\).