Quasi-Polish spaces and spaces of filters in second-order arithmetic

TL;DR

This paper formalizes various representations of quasi-Polish spaces within second-order arithmetic and analyzes their interrelations through reverse mathematics.

Contribution

It provides a systematic reverse mathematical analysis of the equivalences and transitions among different quasi-Polish space representations.

Findings

Multiple representations of quasi-Polish spaces are equivalent within second-order arithmetic.

The paper characterizes the logical strength needed for transitions between these representations.

Abstract

The class of quasi-Polish spaces admits several equivalent representations, including UF spaces, NP spaces, $\mathbf{\Pi}_2^0$ subspaces of $\mathcal{P}(\mathbb{N})$, and sober spaces of countably presented frames. In this paper, we formalize these structures within second-order arithmetic and conduct a systematic reverse mathematical analysis of the transitions between them.