Abstract
We initiate the reverse mathematics of general topology. We show that a certain metrization theorem is equivalent to Π2 1 comprehension. An MF space is defined to be a topological space of the form MF(P) with the topology generated by $\lbrace N_p \mid p \in P \rbrace$ . Here P is a poset, MF(P) is the set of maximal filters on P, and $N_p = \lbrace F \in MF(P) \mid p \in F \rbrace$ . If the poset P is countable, the space MF(P) is said to be countably based. The class of countably based MF spaces can be defined and discussed within the subsystem ACA0 of second order arithmetic. One can prove within ACA0 that every complete separable metric space is homeomorphic to a countably based MF space which is regular. We show that the converse statement, "every countably based MF space which is regular is homeomorphic to a complete separable metric space," is equivalent to Π2 1-CA0. The equivalence is proved in the weaker system Π1 1-CA0. This is the first example of a theorem of core mathematics which is provable in second order arithmetic and implies Π2 1 comprehension