Reverse mathematics and π21 comprehension
Carl Mummert, Stephen G. Simpson · 2005
Abstract. We initiate the reverse mathematics ofgeneraltopology. We show thata certain m etrization theorem is equivalent to Π12 comprehension. An MF space is defined to be a topologicalspace of the form MF(P) with the topology generated by fNp j p 2 Pg. Here P is a poset, MF(P) is the setof maximalfilters on P, and Np = fF 2 MF(P) j p 2 F g. If the posetP 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 orderarithm etic. One can prove within ACA0 that every complete separable m etric space is hom eomorphicto a countably based MF space which is regular. We show thatthe converse statem ent, “every countably basedMF space which is regularis hom eomorphicto a complete separable m etric space, ” is equivalentto Π12-CA0. The equivalence is proved in the weakersystem Π11-CA0. This is the firstexample of a theorem of core mathematics which is provable in second orderarithm eticand im plies Π12 comprehension. In the foundations ofmathematics, there is an ongoingresearch program known as reverse mathematics. One focuses on specific core mathematical theorem s ô, and one determ ines the weakestsetexistence axiom s which are needed in orderto prove ô. Such determ inations are made in the contextof subsystem s ofsecondorderarithm etic, Z2. The strength ofô is m easured by showing that ô is logically equivalentto a particular subsystem of Z2, over a weaker subsystem. The standard reference for reverse mathematics and subsystem s ofZ2 is Sim pson [12]. See also [11]. Previous reverse mathematics studies [12], [11] have included an extensive developm entofthe reverse mathematics ofcomplete separable m etricspaces. We now initiate the reverse mathematics ofgeneraltopologicalspaces. Defi nition 1. The subsystem s ofZ2 used in this paperare ACA0, Π11-CA0, andΠ12-CA0. We brieflydescribe these system s. The language ofZ2 includes numbervariables k;m; n; : : : rangingoverN, the setofnaturalnumbers, and setvariablesX;Y;Z; : : : rangingoversubsets ofN. Allofoursystem s include