Reverse mathematics, well-quasi-orders, and Noetherian spaces (Q283113)

This paper uses techniques of reverse mathematics to analyze the logical strength of theorems related to work of \textit{J. Goubault-Larrecq} [``On Noetherian spaces'', in: Proceedings of the 22nd annual IEEE symposium on logic in computer science, LICS 2007. Los Alamitos, CA: IEEE Computer Society. 453--462 (2007; \url{doi:10.1109/LICS.2007.34})]. Given a quasi-order \(Q\), one can induce quasi-orders on the power set of \(Q\), for example, the Hoare quasi-order \(\mathcal P ^\flat (Q)\) and the Smyth quasi-order \(\mathcal P^\sharp (Q)\). Quasi-orders can be topologized using the Alexandroff topology \(\mathcal A ( Q)\) or the upper topology \(\mathcal U ( Q)\). If \(Q\) is wqo, then each of the following spaces are Noetherian: \(\mathcal A ({\mathcal {P}}^\flat_{\mathrm f} (Q))\), \(\mathcal U (\mathcal P ^\flat_{\mathrm f} (Q))\), \(\mathcal U (\mathcal P^\sharp_{\mathrm f} (Q))\), \(\mathcal U(\mathcal P^\flat (Q))\), and \(\mathcal U (\mathcal P^\sharp (Q))\). The main result of the paper shows that each of the five preceding assertions is equivalent to ACA\(_0\) over the base system RCA\(_0\). The development makes use of the framework for countable second-countable spaces introduced by \textit{F. G. Dorais} [``Reverse mathematics of compact countable second-countable spaces'', Preprint, \url{arXiv:1110.655}]. Since the arguments are formalized in second-order arithmetic, they provide proofs of Goulbault-Larrecq's results that do not rely on category theoretic methods. Related results on the preservation of wqos and bqos in the induced quasi-orders can be found in the work of \textit{A. Marcone} [in: Reverse mathematics 2001. Wellesley, MA: A K Peters; Urbana, IL: Association for Symbolic Logic (ASL). 303--330 (2005; Zbl 1083.03052)].