Reverse mathematics,well-quasi-orders,and Noetherian spaces

A quasi-order Q induces two natural quasi-orders on \({\mathcal{P}(Q)}\), but if Q is a well-quasi-order, then these quasi-orders need not necessarily be well-quasi-orders. Nevertheless, Goubault-Larrecq (Proceedings of the 22nd Annual IEEE Symposium 4 on Logic in Computer Science (LICS’07), pp. 453–462, 2007) showed that moving from a well-quasi-order Q to the quasi-orders on \({\mathcal{P}(Q)}\) preserves well-quasi-orderedness in a topological sense. Specifically, Goubault-Larrecq proved that the upper topologies of the induced quasi-orders on \({\mathcal{P}(Q)}\) are Noetherian, which means that they contain no infinite strictly descending sequences of closed sets. We analyze various theorems of the form “if Q is a well-quasi-order then a certain topology on (a subset of) \({\mathcal{P}(Q)}\) is Noetherian” in the style of reverse mathematics, proving that these theorems are equivalent to ACA₀ over RCA₀. To state these theorems in RCA₀ we introduce a new framework for dealing with second-countable topological spaces.