On the reverse mathematics of general topology

This thesis presents a formalization of general topology in second-order arithmetic. Topological spaces are represented as spaces of filters on partially ordered sets. If P is a poset, let MF( P) be the set of maximal filters on P. Let UF( P) be the set of unbounded filters on P. If X is MF(P) or UF(P), the topology on X has a basis {lcub}Np | p ∈ P{rcub}, where Np = {lcub}F ∈ X | p ∈ F{rcub}. Spaces of the form MF(P) are called MF spaces; spaces of the form UF(P) are called UF spaces. A poset space is either an MF space or a UF space; a poset space formed from a countable poset is said to be countably based. The class of countably based poset spaces includes all complete separable metric spaces and many nonmetrizable spaces including the Gandy-Harrington space. All poset spaces have the strong Choquet property.; This formalization is used to explore the Reverse Mathematics of general topology. The following results are obtained.; RCA0 proves that countable products of countably based MF spaces are countably based MF spaces. The statement that every Gdelta subspace of a countably based MF space is a countably based MF space is equivalent to P11 -CA0 over RCA0.; The statement that every regular countably based MF space is metrizable is provable in P12 -CA0 and implies ACA 0 over RCA0. The statement that every regular MF space is completely metrizable is equivalent to P12 -CA0 over P11 -CA0. The corresponding statements for UF spaces are provable in P11 -CA0, and each implies ACA 0 over RCA0.; The statement that every countably based Hausdorff UF space is either countable or has a perfect subset is equivalent to ATR 0 over ACA0. P12 -CA0 proves that every countably based Hausdorff MF space has either countably many or continuum-many points; this statement implies ATR0 over ACA0. The statement that every closed subset of a countably based Hausdorff MF space is either countable or has a perfect subset is equivalent over P11 -CA0 to the statement that ℵLA1 is countable for all A ⊆ N .