Reverse Mathematics and Comprehension
Carl Mummert^{1} and Stephen G.
Simpson^{2}
Department of Mathematics
First draft: March 29, 2005
This draft: October 17, 2005
Pennsylvania State University
Bulletin of Symbolic Logic, volume 11, 2005, pp. 526533.
Abstract:
We initiate the reverse mathematics of general topology. We show
that a certain metrization theorem is equivalent to
comprehension. An
MF space is defined to be a topological
space of the form
with the topology generated by
. Here
is a poset,
is the set of maximal
filters on
, and
. If the poset
is countable, the space
is said to be
countably
based. The class of countably based MF spaces can be defined and
discussed within the subsystem
of second order arithmetic.
One can prove within
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

. The
equivalence is proved in the weaker system

. This
is the first example of a theorem of core mathematics which is
provable in second order arithmetic and implies
comprehension.
In the foundations of mathematics, there is an ongoing research
program known as reverse mathematics. One focuses on specific
core mathematical theorems , and one determines the weakest set
existence axioms which are needed in order to prove . Such
determinations are made in the context of subsystems of second order
arithmetic, . The strength of is measured by showing
that is logically equivalent to a particular subsystem of
, over a weaker subsystem. The standard reference for reverse
mathematics and subsystems of is Simpson [12]. See
also [11].
Previous reverse mathematics studies [12,11] have included
an extensive development of the reverse mathematics of complete
separable metric spaces. We now initiate the reverse mathematics of
general topological spaces.
Definition 1
The subsystems of
used in this paper are
,

, and

. We briefly describe these
systems. The language of
includes
number variables
ranging over
, the set of natural numbers, and
set variables ranging over subsets of
.
All of our systems include first order arithmetic plus the induction
axiom
The system
includes
comprehension axioms
where the formula
does not mention
and is
arithmetical, i.e., it contains no set quantifiers. The
system

includes comprehension for formulas
which are
, i.e., of the form
where
is arithmetical. The system

includes comprehension for formulas
which are
, i.e., of the form
where
is arithmetical. In each of
these systems,
is allowed to mention
parameters,
i.e., free set variables. Details concerning these systems are in
[
12, Sections I.1I.6].
Remark 1
In the following definitions, we shall show how to formalize some
key concepts of general topology within
. As is usual in
reverse mathematics (see for example the discussion of complete
separable metric spaces in [
12, Sections II.5II.6]), we
shall employ ``coding'' via definitional extensions of the language
of
. In each case, the ``code'' is a natural number or a set
of natural numbers, but the encoded object may be uncountable. It
will be always be clear how to convert our informal ``coding''
definitions into precise, rigorous, definitional extensions of
.
Definition 2
A
poset is a partially ordered set. Within
, let
be a countable poset. A
filter^{3} on
is a set
such that (1) for
all
and
we have
, and (2) for all
there exists
such that
and
. A
maximal filter is a filter which is not included in any
larger filter. Within
, consider the topological space
whose points are the maximal filters on
, and whose
basic open sets are
for all
. Such a space is called a
countably based MF
space. See also Mummert [
8,
9].
Remark 2
In Definition
2 within
, the countable poset
is regarded as a code for the topological space
, and each
is regarded as a code for the basic open neighborhood
in
. In general, the open sets of
are of the form
where
is a subset of
. Thus, if
is a
point of
, i.e., a maximal filter on
, then we have
if
and only if
, and
if and only if
. Thus the countable set
may be
regarded as a code for the open set
.
Definition 3
Within
, if
is a countable pseudometric space, let
be the complete separable metric space
whose points are the equivalence classes of Cauchy sequences in
, two such sequences
and
being equivalent if and only if
. Clearly all complete separable metric spaces
arise in this way. See also [
12, Sections I.4, II.5II.7, III.2,
IV.1IV.2]. Given
as above, consider also the
countable poset
where
is the set of positive rational numbers, partially
ordered by putting
if and only if
. One
can show in
(see [
8, Sections 2.3.1 and
3.2] and [
9]) that there is a
canonically arithmetically definable, onetoone correspondence
between the points of
and the maximal
filters on
. Moreover, a point
belongs
to a basic open ball
if and only if the corresponding maximal filter belongs to
. Thus, in the topological context, we are justified in
identifying the complete separable metric space
with the countably based MF space
, where
.
Definition 4
Within
, if
and
are countable posets, we define a
code for a continuous function from to to
be a set
such that, for all maximal
filters
on
,
is a maximal filter on
. It can be shown that each such code
induces a continuous function
. Moreover, all
continuous functions from
to
are induced by such
codes. A
homeomorphism from to is a coded
continuous
together with a coded continuous
inverse
. The requirement of a coded
continuous inverse is apparently not superfluous; we do not know
whether it is provable in

that every coded
continuous open bijection
has a coded
continuous inverse. See also [
8, Section 3.2.3]
and [
9].
Remark 3
We offer the following reasons for focusing on the class of
countably based MF spaces. See also Mummert
[
8,
9].
 In earlier reverse mathematics studies (see
[12,11]), the restriction to subsystems of has
been appropriate, natural, and fruitful. Therefore, in order to
extend reverse mathematics to general topology, it is important to
identify a class of topological spaces which is reasonably broad
yet conveniently formalizable in . It turns out that the
countably based MF spaces are just such a class.
 As already noted in Definition 3, the class of
countably based MF spaces includes all complete separable metric
spaces. Thus, it includes many of the topological spaces which
arise in core mathematical disciplines such as analysis and
geometry.
 In addition, the class of countably based MF spaces includes
many topological spaces which are not metrizable. An interesting
example is the Gandy/Harrington space (see
[3, p. 240]), which is well known to be of great
importance in contemporary descriptive set theory
[1,4]. See also [8, Section
2.3.4] and [9].
 The class of countably based MF spaces enjoys some nice
closure properties. First, the product of countably many
countably based MF spaces is homeomorphic to a countably based MF
space. Second, any nonempty set^{4} in a
countably based MF space is homeomorphic to a countably based MF
space. See also [8, Section 2.3.2] and
[9].
Definition 5
A topological space is said to be
regular if, for every open
set
and point
, there exists an open set
such that
and the closure of
is included in
. See for example
Kelley [
5, page 113]. It is well known and easy to see
that metric spaces are regular.
Definition 6
We study the reverse mathematics of the following metrization
theorem for countably based MF spaces.
MFMT: A countably based MF space is homeomorphic to a complete
separable metric space if and only if it is regular.
Proof.One direction of MFMT is easy. It is straightforward to prove in
that every countably based MF space which is homeomorphic
to a complete separable metric space is regular.
In the other direction, we prove within  that every
countably based MF space which is regular is homeomorphic to a
complete separable metric space. Our argument is loosely based on
the original proofs of the metrization theorems due to Urysohn (see
also Schröder [10]) and Choquet (see
also Kechris [3, Section 8.E]). The details of our
argument are in Mummert [8, Section 4.3] and
[9]. Here we provide only a sketch.
Reasoning within , let be a countable poset such
that is regular. We use comprehension to form
the set of ordered pairs
such that
includes the closure of . Using this set as a parameter, we
adapt a construction of Schröder in effective topology
[10] to obtain a metric on which is
compatible with the topology of . Thus is
metrizable, but we have not yet shown that is completely
metrizable.
Fix a countable dense set
. We use
comprehension to form the sets
and
where
. Using these sets as
parameters, we attempt to imitate the proof of Choquet's theorem
(see [3, Section 8.E]) that any metric space having
the strong Choquet property is completely metrizable. It is
provable in (see [8, Theorem 2.3.29] and
[9]) that every MF space has the strong Choquet
property, but unfortunately this gametheoretic property is not
definable in . We overcome this obstacle by giving a direct
proof within  that every countably based MF space
which is metrizable is completely metrizable. The details are in
[8, Section 4.3] and [9].
In this way we obtain a complete metric on which is
compatible with and hence compatible with the topology of
. It is then straightforward using comprehension
to construct a homeomorphism between and
where . This
proves our lemma.
Theorem 1
The following are equivalent over

.
 comprehension.
 MFMT.
Proof.Lemma 1 shows that comprehension implies
MFMT. It remains to prove the reversal. We work in
 and assume MFMT. Consider a formula
where is . In order to
prove comprehension, it suffices to prove the existence of
the set
. By Kondo's
uniformization theorem (provable in , see
[12, Section VI.2]), we may safely assume that for each
there exists at most one , call it , such that
holds.
We write in normal form as
. Here we are using the finite sequence notation
and
. We may safely assume that
holds. For finite sequences
and , we write
if and only if
is a proper initial segment of . Let be the
countable poset consisting of all ordered triples
such that
holds, plus all ordered
pairs , partially ordered as follows:

if and only if and
and
.

if and only if and
.

if and only if and
.

never.
The maximal filters on are of three types:

where is a minimal element of
.

where are
such that
holds.

where is such that
.
Note that there is a closed set
consisting of
for all such that
holds. The
complement of is the open set
.
We claim that is regular. Clearly it will suffice to show
that, for all maximal filters and basic open sets such
that , we can find a basic open set such that and the closure of is included in . We shall find
such an with the additional property that is closed.
Thus we shall see that the topology of is generated by
basic open sets which are also closed.
Case 1:
where is a minimal element of
. In this case is an isolated point of , and
is closed. For use in cases 2 and 3, let be the
open set consisting of these isolated points, i.e.,
where is the set of minimal elements of .
Case 2:
where are
such that
holds. It follows that
fails. Hence if exists. Suppose , i.e., . If , then is closed,
because the complement of is the open set
where is the set of
such that or
. If
, let be so large
that
if exists, and put
.
Then
. Moreover, is closed, because
the complement of is the open set
where is the set of such that or
, and is the set of
such that or or .
Case 3: . In this case, for all such that ,
we have for some . As in case 2, is closed.
We have now proved that is regular. It follows by MFMT
that there exists a homeomorphism of onto a complete
separable metric space
. In
particular, since is a closed set in , is a
closed set in
. For each
, if
exists then is the unique point of
, hence
is the
unique point of
. If
does not exist, then
, hence
. Note also that
the sequence of open sets
,
, is
arithmetically definable uniformly in , using the code of
as a parameter. Thus we can use comprehension
to form the set
This completes the proof.
Remark 4
Theorem
1 shows that a certain metrization theorem is
logically equivalent to

over

. We
believe that this is the first convincing instance of a core
mathematical theorem which is equivalent to
comprehension,
in the sense of reverse mathematics. Previous reverse mathematics
results within
(see [
12,
11]) have involved only
set existence axioms which are strictly weaker than
comprehension.
^{5}
 1

Leo A. Harrington, Alexander S. Kechris, and Alain Louveau.
A GlimmEffros dichotomy for Borel equivalence relations.
Journal of the American Mathematical Society, 3:903928, 1990.
 2

Christoph Heinatsch and Michael Möllerfeld.
The determinacy strength of comprehension.
Preprint, 11 pages, February 10, 2005, submitted for publication.
 3

Alexander S. Kechris.
Classical Descriptive Set Theory.
Graduate Texts in Mathematics. SpringerVerlag, 1985.
XVIII + 402 pages.
 4

Alexander S. Kechris and Alain Louveau.
The classification of hypersmooth Borel equivalence relations.
Journal of the American Mathematical Society, 10:215242,
1997.
 5

John L. Kelley.
General Topology.
Van Nostrand, 1955.
XIV + 298 pages.
 6

K. Ko, A. Nerode, M. B. PourEl, K. Weihrauch, and J. Wiedermann, editors.
Computability and Complexity in Analysis, volume 235 of InformatikBerichte.
Fernuniversität Hagen, August 1998.
 7

Kenneth Kunen.
Set Theory, an Introduction to Independence Proofs.
Studies in Logic and the Foundations of Mathematics.
NorthHolland, 1980.
XVI + 313 pages.
 8

Carl Mummert.
On the Reverse Mathematics of General Topology.
PhD thesis, The Pennsylvania State University, 2005.
VI + 102 pages.
 9

Carl Mummert.
Reverse mathematics of MF spaces.
In preparation, 2005.
 10

Matthias Schröder.
Effective metrization of regular spaces.
In [6], pages 6380, 1998.
 11

S. G. Simpson, editor.
Reverse Mathematics 2001, volume 21 of Lecture Notes
in Logic.
Association for Symbolic Logic, 2005.
VIII + 401 pages.
 12

Stephen G. Simpson.
Subsystems of Second Order Arithmetic.
Perspectives in Mathematical Logic. SpringerVerlag, 1999.
XIV + 445 pages.
Reverse Mathematics and Comprehension
This document was generated using the
LaTeX2HTML translator Version 200221 (1.71)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html split 0 pi12
The translation was initiated by Stephen G Simpson on 20051017
Footnotes
 ... Mummert^{1}
 mummert@math.psu.edu,
http://www.math.psu.edu/mummert/. Mummert's research was
partially supported by a VIGRE graduate traineeship under NSF
Grant DMS9810759.
 ... Simpson^{2}
 t20@psu.edu,
http://www.personal.psu.edu/t20/. Simpson's research was
partially supported by NSF Grant DMS0070718. We thank the
referee for comments which led to improvements in this paper.
 ...filter^{3}
 Our notion of a
filter on a poset is identical to the one that is often used in
forcing in axiomatic set theory. See for example Kunen
[7].
 ... set^{4}
 In the
context of arbitrary topological spaces, a set
is defined to be the intersection of countably many open sets.
In metric spaces, it is easy to see that every closed set is a
set, but unfortunately this result does not
generalize to arbitrary topological spaces, or even to arbitrary
countably based MF spaces. As an example in the
Gandy/Harrington space, we may take any lightface set
which is not boldface . See also [8, proof of
Theorem 2.3.40] and [9].
 ... comprehension.^{5}
 However, Heinatsch and Möllerfeld
[2] have shown that  proves the same
sentences as
plus 
determinacy, i.e., determinacy for Boolean combinations of
sets in the Baire space.
Stephen G Simpson
20051017