# Reverse Mathematics and Comprehension

Carl Mummert1 and Stephen G. Simpson2

Department of Mathematics

First draft: March 29, 2005
This draft: October 17, 2005

Pennsylvania State University

Bulletin of Symbolic Logic, volume 11, 2005, pp. 526-533.

### 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.1-I.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.5-II.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 filter3 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.5-II.7, III.2, IV.1-IV.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, one-to-one 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].
1. 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.
2. 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.
3. 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].
4. 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 set4 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.

Lemma 1   MFMT is provable in -.

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 game-theoretic 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 -.
1. comprehension.
2. 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:

1. if and only if and and .
2. if and only if and .
3. if and only if and .
4. never.
The maximal filters on are of three types:
1. where is a minimal element of .
2. where are such that holds.
3. 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

## Bibliography

1
Leo A. Harrington, Alexander S. Kechris, and Alain Louveau.
A Glimm-Effros dichotomy for Borel equivalence relations.
Journal of the American Mathematical Society, 3:903-928, 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. Springer-Verlag, 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:215-242, 1997.

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

6
K. Ko, A. Nerode, M. B. Pour-El, K. Weihrauch, and J. Wiedermann, editors.
Computability and Complexity in Analysis, volume 235 of Informatik-Berichte.
Fernuniversität Hagen, August 1998.

7
Kenneth Kunen.
Set Theory, an Introduction to Independence Proofs.
Studies in Logic and the Foundations of Mathematics. North-Holland, 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 63-80, 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. Springer-Verlag, 1999.
XIV + 445 pages.

Reverse Mathematics and Comprehension

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (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 2005-10-17

#### Footnotes

... Mummert1
mummert@math.psu.edu, http://www.math.psu.edu/mummert/. Mummert's research was partially supported by a VIGRE graduate traineeship under NSF Grant DMS-9810759.
... Simpson2
t20@psu.edu, http://www.personal.psu.edu/t20/. Simpson's research was partially supported by NSF Grant DMS-0070718. We thank the referee for comments which led to improvements in this paper.
...filter3
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].
... set4
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 2005-10-17