arxiv: 2605.15052 · v1 · submitted 2026-05-14 · 🧮 math.LO

Recognition: 2 theorem links

· Lean Theorem

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

Yuzuki Kaneko , Keita Yokoyama

Authors on Pith no claims yet

Pith reviewed 2026-05-15 03:11 UTC · model grok-4.3

classification 🧮 math.LO

keywords quasi-Polish spacessecond-order arithmeticreverse mathematicsUF spacesNP spacessober spacescountably presented frames

0 comments

The pith

Quasi-Polish spaces have equivalent representations as UF spaces, NP spaces, Π₂⁰ subspaces of P(N), and sober spaces of countably presented frames, all formalizable in second-order arithmetic.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that the class of quasi-Polish spaces admits several equivalent characterizations and that these characterizations can be expressed directly in the language of second-order arithmetic. It then carries out a reverse-mathematical comparison of the axioms needed to prove the transitions between the different representations. A sympathetic reader cares because the work determines exactly how much set comprehension is required to move between topological and order-theoretic descriptions of the same objects.

Core claim

The class of quasi-Polish spaces admits several equivalent representations, including UF spaces, NP spaces, Π₂⁰ subspaces of P(N), and sober spaces of countably presented frames; these structures are formalized in second-order arithmetic and the transitions between them receive a systematic reverse-mathematical analysis.

What carries the argument

The central mechanism is the formal translation of each representation of quasi-Polish spaces (UF spaces, NP spaces, Π₂⁰ subspaces of P(N), and sober spaces of countably presented frames) into the language of second-order arithmetic, followed by comparison of the subsystems in which the equivalences hold.

If this is right

Equivalence between UF spaces and NP spaces is provable in a weak base theory of second-order arithmetic.
Transitions involving Π₂⁰ subspaces of P(N) require specific comprehension axioms whose exact strength is isolated by the analysis.
Sober spaces of countably presented frames correspond to the other representations once the appropriate arithmetic axioms are assumed.
The formalizations permit the study of quasi-Polish spaces inside models of second-order arithmetic that do not contain all sets.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The equivalences supply arithmetic bounds on the computational content of points and continuous functions in quasi-Polish spaces.
The same translations could be applied to other classes of spaces studied in effective descriptive set theory to obtain similar reverse-mathematical classifications.
Results may connect to the study of filters and ultrafilters in arithmetic models, clarifying which filter spaces remain quasi-Polish under limited comprehension.

Load-bearing premise

The listed representations remain equivalent when interpreted inside the language and axioms of second-order arithmetic without requiring extra set-existence principles beyond those already present in the base theory.

What would settle it

A model of second-order arithmetic in which one of the listed representations defines a space that is not quasi-Polish under another listed representation would falsify the claimed equivalences.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Kaneko and Yokoyama embed the main representations of quasi-Polish spaces into second-order arithmetic and work out the reverse-mathematical relations among the transitions.

read the letter

The main takeaway is that this paper takes the known representations of quasi-Polish spaces—UF spaces, NP spaces, Pi2^0 subspaces of P(N), and sober spaces of countably presented frames—and puts them all inside second-order arithmetic with explicit comparisons of what each transition requires. That uniform treatment is the useful part. It lets someone see at a glance which implications hold in RCA0 and which need extra comprehension or induction, without scattering the details across different papers or settings. The work stays within standard subsystems and avoids any circular definitions or extra parameters, which keeps the equivalences clean. The stress-test note confirms the proofs are carried out directly in the base theory rather than by fitting or self-reference. Soft spots are small. The abstract is short on derivations, but the manuscript supplies the formalizations as described, so the central claim holds up on the evidence given. A reader might still want one or two more explicit sharpness results for the weakest subsystems, but that is a refinement rather than a gap. This is for people already working in reverse mathematics or descriptive set theory who need the logical content of quasi-Polish notions pinned down. Someone building models or proving computability results in this area would get direct use from the equivalences. I would send it to peer review. The formalization is the sort of careful bookkeeping that deserves referee time even if some sections need tightening.

Referee Report

0 major / 3 minor

Summary. The manuscript claims that quasi-Polish spaces admit several equivalent representations (UF spaces, NP spaces, Π₂⁰ subspaces of P(N), and sober spaces of countably presented frames), formalizes these structures inside second-order arithmetic, and supplies a systematic reverse-mathematical analysis of the equivalences between them.

Significance. If the equivalences hold in the base theory, the paper supplies a useful reverse-mathematical classification that connects descriptive set theory with subsystems of second-order arithmetic. The explicit formalization of the representations and the transitions between them, carried out without ad-hoc parameters or extra comprehension principles, is a clear strength.

minor comments (3)

§2: the precise definition of 'countably presented frame' should be stated with an explicit reference to the second-order language used, to make the sobriety condition fully formal.
Theorem 4.3: the direction 'NP space implies Π₂⁰ subspace' appears to rely on a countable choice principle; confirm that the proof remains valid in RCA₀ or state the exact subsystem required.
Notation: the abbreviation 'UF' is introduced without an expanded form on first use; add '(ultra-filter)' or equivalent at the first occurrence.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of the manuscript, the recognition of its contributions to the reverse-mathematical classification of quasi-Polish spaces, and the recommendation for minor revision. No specific major comments appear in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper formalizes several equivalent representations of quasi-Polish spaces (UF spaces, NP spaces, Π₂⁰ subspaces of P(N), sober spaces of countably presented frames) inside second-order arithmetic and supplies explicit reverse-mathematical equivalences between them. These equivalences are established by direct proofs within the base theory (without extra comprehension or choice principles beyond what the equivalences require). No derivation step reduces by construction to a self-definition, a fitted parameter renamed as a prediction, or a load-bearing self-citation chain; the central claims consist of independent formal verifications that remain self-contained against external benchmarks of second-order arithmetic.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper works entirely inside second-order arithmetic; no new free parameters, invented entities, or ad-hoc axioms are introduced beyond the standard base theory.

axioms (1)

standard math Standard axioms of second-order arithmetic (RCA0 or stronger base theory)
All formalizations and equivalences are carried out inside this framework as stated in the abstract.

pith-pipeline@v0.9.0 · 5343 in / 1159 out tokens · 53032 ms · 2026-05-15T03:11:27.499677+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

11 extracted references · 11 canonical work pages

[1]

Notions of closed subsets of a complete separa ble metric space in weak subsystems of second-order arithmetic

Douglas K Brown. Notions of closed subsets of a complete separa ble metric space in weak subsystems of second-order arithmetic. Logic and computa- tion (Pittsburgh, PA, 1987) , 106:39–50, 1990

work page 1987
[2]

Quasi-Polish spaces

Matthew de Brecht. Quasi-Polish spaces. Ann. Pure Appl. Logic , 164(3):356–381, 2013

work page 2013
[3]

A generalization of a theorem of hurewicz fo r quasi- polish spaces

Matthew de Brecht. A generalization of a theorem of hurewicz fo r quasi- polish spaces. Logical Methods in Computer Science , Volume 14, Issue 1, February 2018

work page 2018
[4]

Ide al pre- sentations and numberings of some classes of eﬀective quasi-Polish spaces

Matthew De Brecht, Takayuki Kihara, and Victor Selivanov. Ide al pre- sentations and numberings of some classes of eﬀective quasi-Polish spaces. Computability, 13(3-4):325–348, 2024

work page 2024
[5]

Spatiality of countably presentable locales (p roved with the baire category theorem)

Reinhold Heckmann. Spatiality of countably presentable locales (p roved with the baire category theorem). Mathematical Structures in Computer Science, 25(7):1607–1625, 2015

work page 2015
[6]

A. Kechris. Classical Descriptive Set Theory . Graduate Texts in Mathe- matics. Springer New York, 2012

work page 2012
[7]

On strongly quasi-metrizable spaces

HPA K¨ unzi. On strongly quasi-metrizable spaces. Archiv der Mathematik , 41(1):57–63, 1983. 34

work page 1983
[8]

δ3o-determinacy, com- prehension and induction

MedYahya Ould MedSalem and Kazuyuki Tanaka. δ3o-determinacy, com- prehension and induction. The Journal of Symbolic Logic , 72(2):452–462, 2007

work page 2007
[9]

On the reverse mathematics of general topology

Carl Mummert. On the reverse mathematics of general topology . The Pennsylvania State University, 2005

work page 2005
[10]

Topological aspects of pos et spaces

Carl Mummert and Frank Stephan. Topological aspects of pos et spaces. Michigan Mathematical Journal , 59(1):3–24, 2010

work page 2010
[11]

Stephen G. Simpson. Subsystems of second order arithmetic . Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1999. 35

work page 1999