Reverse Mathematics and Π_{2}^{1} Comprehension

Carl Mummert^{∗} and Stephen G. Simpson^{†} Department of Mathematics Pennsylvania State University University Park, State College PA, 16802

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

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 Π_{2}^{1} comprehension. An MF space is defined to be a topological space of the form MF(P) with the topology generated by {N_{p} | p ∈ P }. Here P is a poset, MF(P) is the set of maximal filters on P, and N_{p} = {F ∈ MF(P) | p ∈ F }. 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 ACA_{0} of second order arithmetic. One can prove within ACA_{0} 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}-CA_{0}. The equivalence is proved in the weaker system Π_{1}^{1}-CA_{0}. This is the first example of a theorem of core mathematics which is provable in second order arithmetic and implies Π_{2}^{1} 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, Z_{2}. The strength of τ is measured by showing that τ is logically equivalent to a particular subsystem of Z_{2}, over a weaker subsystem. The standard reference for reverse mathematics and subsystems of Z_{2} is Simpson [12]. See also [11].

∗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.

†simpson@math.psu.edu, http://www.math.psu.edu/simpson/. Simpson’s research was partially supported by NSF Grant DMS-0070718. We thank the referee for comments which led to improvements in this paper.

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 Z_{2} used in this paper are ACA_{0}, Π_{1}^{1}-CA_{0}, and Π_{2}^{1}-CA_{0}. We briefly describe these systems. The language of Z_{2} includes number variables k, m, n, … ranging over ℕ, the set of natural numbers, and set variables X, Y, Z, … ranging over subsets of ℕ. All of our systems include first order arithmetic plus the induction axiom

∀X [ (0 ∈ X ∧ ∀n (n ∈ X ⇒ n + 1 ∈ X)) ⇒ ∀n (n ∈ X) ] .

The system ACA_{0} includes comprehension axioms

∃X ∀n [ n ∈ X ⇔ φ(n) ]

where the formula φ(n) does not mention X and is arithmetical, i.e., it contains no set quantifiers. The system Π_{1}^{1}-CA_{0} includes comprehension for formulas φ(n) which are Π_{1}^{1}, i.e., of the form ∀Y θ(n, Y) where θ(n, Y) is arithmetical. The system Π_{2}^{1}-CA_{0} includes comprehension for formulas φ(n) which are Π_{2}^{1}, i.e., of the form ∀Y ∃Z θ(n, Y, Z) where θ(n, Y, Z) is arithmetical. In each of these systems, φ(n) 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 ACA_{0}. 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 Z_{2}. 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 ACA_{0}.

Definition 2. A poset is a partially ordered set. Within ACA_{0}, let P be a countable poset. A filter^{1} on P is a set F ⊆ P such that (1) for all p ∈ F and q ≥ p we have q ∈ F, and (2) for all p, q ∈ F there exists r ∈ F such that p ≥ r and q ≥ r. A maximal filter is a filter which is not included in any larger filter. Within ACA_{0}, consider the topological space MF(P) whose points are the maximal filters on P, and whose basic open sets are

N_{p} = {F ∈ MF(P) | p ∈ F }

for all p ∈ P. Such a space is called a countably based MF space. See also Mummert [8, 9].

1Our 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].

Remark 2. In Definition 2 within ACA_{0}, the countable poset P is regarded as a code for the topological space MF(P), and each p ∈ P is regarded as a code for the basic open neighborhood N_{p} in MF(P). In general, the open sets of MF(P) are of the form

U_{L} = ⋃_{p∈L} N_{p} = {F ∈ MF(P) | ∃p ∈ L [ F ∈ N_{p}] }

where L is a subset of P. Thus, if F is a point of MF(P), i.e., a maximal filter on P, then we have F ∈ N_{p} if and only if p ∈ F, and F ∈ U_{L} if and only if F ∩ L ≠ ∅. Thus the countable set L ⊆ P may be regarded as a code for the open set U_{L} ⊆ MF(P).

Definition 3. Within ACA_{0}, if (A, d) is a countable pseudometric space, let (Â, d̂) be the complete separable metric space whose points are the equivalence classes of Cauchy sequences in (A, d), two such sequences ⟨a_{n} | n ∈ ℕ⟩ and ⟨b_{n} | n ∈ ℕ⟩ being equivalent if and only if lim_{n} d(a_{n}, b_{n}) = 0. 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 (A, d) as above, consider also the countable poset

P_{(A,d)} = A × ℚ^{+}

where ℚ^{+} is the set of positive rational numbers, partially ordered by putting (a, r) < (b, s) if and only if d(a, b)+r < s. One can show in ACA_{0} (see [8, Sections 2.3.1 and 3.2] and [9]) that there is a canonically arithmetically definable, oneto-one correspondence between the points of (Â, d̂) and the maximal filters on P_{(A,d)}. Moreover, a point x ∈ Â belongs to a basic open ball

B(a, r) = {x ∈ Â | d̂(a, x) < r}

if and only if the corresponding maximal filter belongs to N_{(a,r)}. Thus, in the topological context, we are justified in identifying the complete separable metric space (Â, d̂) with the countably based MF space MF(P), where P = P_{(A,d)}.

Definition 4. Within ACA_{0}, if P and Q are countable posets, we define a code for a continuous function from MF(P) to MF(Q) to be a set Φ ⊆ P × Q such that, for all maximal filters F on P,

Φ(F) = {q ∈ Q | ∃p ∈ F [ (p, q) ∈ Φ ] }

is a maximal filter on Q. It can be shown that each such code induces a continuous function Φ : MF(P) → MF(Q). Moreover, all continuous functions from MF(P) to MF(Q) are induced by such codes. A homeomorphism from MF(P) to MF(Q) is a coded continuous Φ : MF(P) → MF(Q) together with a coded continuous inverse Φ^{−1} : MF(Q) → MF(P). The requirement of a coded continuous inverse is apparently not superfluous; we do not know whether it is provable in Π_{2}^{1}-CA_{0} that every coded continuous open bijection Φ : MF(P) → MF(Q) 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 Z_{2} 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 Z_{2}. 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 G_{δ} set^{2} 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 U and point x ∈ U, there exists an open set V such that x ∈ V and the closure of V is included in U. 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 Π_{2}^{1}-CA_{0}.

Proof. One direction of MFMT is easy. It is straightforward to prove in ACA_{0} that every countably based MF space which is homeomorphic to a complete separable metric space is regular.

2In the context of arbitrary topological spaces, a G_{δ} 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 G_{δ} 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 Π_{1}^{1} set which is not boldface Σ_{1}^{1}. See also [8, proof of Theorem 2.3.40] and [9].

In the other direction, we prove within Π_{2}^{1}-CA_{0} 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 Π_{2}^{1}-CA_{0}, let P be a countable poset such that MF(P) is regular. We use Π_{2}^{1} comprehension to form the set of ordered pairs (p, q) ∈ P ×P such that N_{p} includes the closure of N_{q}. Using this set as a parameter, we adapt a construction of Schröder in effective topology [10] to obtain a metric d_{1} on MF(P) which is compatible with the topology of MF(P). Thus MF(P) is metrizable, but we have not yet shown that MF(P) is completely metrizable.

Fix a countable dense set A ⊆ MF(P). We use Π_{2}^{1} comprehension to form the sets

{(a, r, p) ∈ A × ℚ^{+} × P | B_{1}(a, r) ⊆ N_{p}}

and

{(a, r, p) ∈ A × ℚ^{+} × P | N_{p} ⊆ B_{1}(a, r)}

where B_{1}(a, r) = {x ∈ MF(P) | d_{1}(a, x) < r}. 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 ZFC (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 Z_{2}. We overcome this obstacle by giving a direct proof within Π_{2}^{1}-CA_{0} 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 d_{2} on MF(P) which is compatible with d_{1} and hence compatible with the topology of MF(P). It is then straightforward using Π_{2}^{1} comprehension to construct a homeomorphism between MF(P) and (Â, d̂_{2}) = MF(Q) where Q = P_{(A,d_{2})}. This proves our lemma. □

Theorem 1. The following are equivalent over Π_{1}^{1}-CA_{0}.

1. Π_{2}^{1} comprehension.

2. MFMT.

Proof. Lemma 1 shows that Π_{2}^{1} comprehension implies MFMT. It remains to prove the reversal. We work in Π_{1}^{1}-CA_{0} and assume MFMT. Consider a Σ_{2}^{1} formula ∃X ψ(n, X) where ψ(n, X) is Π_{1}^{1}. In order to prove Π_{2}^{1} comprehension, it suffices to prove the existence of the set S = {n ∈ ℕ | ∃X ψ(n, X)}. By Kondo’s Π_{1}^{1} uniformization theorem (provable in Π_{1}^{1}-CA_{0}, see [12, Section VI.2]), we may safely assume that for each n there exists at most one X, call it X_{n}, such that ψ(n, X) holds.

We write ψ(n, X) in normal form as ¬ ∃f ∀m R(n, X[m], f[m]). Here we are using the finite sequence notation X[m] = ⟨X(0), …, X(m − 1)⟩ and f[m] = ⟨f(0), …, f(m−1)⟩. We may safely assume that ∀n R(n, ⟨⟩, ⟨⟩) holds. For finite sequences σ and τ, we write σ ⊃ τ if and only if τ is a proper initial segment of σ. Let P be the countable poset consisting of all ordered triples (n, X[k], f[k]) such that (∀m ≤ k) R(n, X[m], f[m]) holds, plus all ordered pairs (n, X[k]), partially ordered as follows:

1. (n, X[k], f[k]) < (n′, X′[k′], f′[k′]) if and only if n = n′ and X[k] ⊃ X′[k′] and f[k] ⊃ f′[k′].

2. (n, X[k]) < (n′, X′[k′]) if and only if n = n′ and X[k] ⊃ X′[k′].

3. (n, X[k], f[k]) < (n′, X′[k′]) if and only if n = n′ and X[k] ⊃ X′[k′].

4. (n, X[k]) < (n′, X′[k′], f′[k′]) never.

The maximal filters F on P are of three types:

1. F = {p ∈ P | q ≤ p} where q is a minimal element of P.

2. F = {(n, X[k], f[k]), (n, X[k]) | k ∈ ℕ} where n, X, f are such that ∀m R(n, X[m], f[m]) holds.

3. F = F_{n} = {(n, X_{n}[k]) | k ∈ ℕ} where n is such that ∃X ψ(n, X).

Note that there is a closed set C ⊆ MF(P) consisting of F_{n} for all n such that ∃X ψ(n, X) holds. The complement of C is the open set ⋃_{n∈ℕ} N_{(n,⟨⟩,⟨⟩)}.

We claim that MF(P) is regular. Clearly it will suffice to show that, for all maximal filters F and basic open sets N_{p} such that F ∈ N_{p}, we can find a basic open set N_{q} such that F ∈ N_{q} and the closure of N_{q} is included in N_{p}. We shall find such an N_{q} with the additional property that N_{q} is closed. Thus we shall see that the topology of MF(P) is generated by basic open sets which are also closed.

Case 1: F = {p ∈ P | q ≤ p} where q is a minimal element of P. In this case F is an isolated point of MF(P), and N_{q} = {F } is closed. For use in cases 2 and 3, let W be the open set consisting of these isolated points, i.e.,

W = ⋃_{q∈M} N_{q}

where M is the set of minimal elements of P.

Case 2: F = {(n, X[k], f[k]), (n, X[k]) | k ∈ ℕ} where n, X, f are such that ∀m R(n, X[m], f[m]) holds. It follows that ψ(n, X) fails. Hence X ≠ X_{n} if X_{n} exists. Suppose F ∈ N_{p}, i.e., p ∈ F. If p = (n, X[k]), then N_{p} is closed, because the complement of N_{p} is the open set

(W \ N_{p}) ∪ ⋃_{p′∈L′} N_{p′}

where L′ is the set of p′ = (n′, X′[k]) ∈ P such that n′ ≠ n or X′[k] ≠ X[k]. If p = (n, X[k], f[k]), let m ≥ k be so large that X[m] ≠ X_{n}[m] if X_{n} exists, and put q = (n, X[m], f[m]). Then F ∈ N_{q} ⊆ N_{p}. Moreover, N_{q} is closed, because the complement of N_{q} is the open set

(W \ N_{q}) ∪ ⋃_{p′∈L′′} N_{p′} ∪ ⋃_{q′∈M′′} N_{q′}

where L′′ is the set of p′ = (n′, X′[m]) such that n′ ≠ n or X′[m] ≠ X[m], and M′′ is the set of q′ = (n′, X′[m], f′[m]) ∈ P such that n′ ≠ n or X′[m] ≠ X[m] or f′[m] ≠ f[m].

Case 3: F = F_{n}. In this case, for all N_{p} such that F ∈ N_{p}, we have p = (n, X_{n}[k]) for some k. As in case 2, N_{p} is closed.

We have now proved that MF(P) is regular. It follows by MFMT that there exists a homeomorphism Φ of MF(P) onto a complete separable metric space (Â, d̂). In particular, since C is a closed set in MF(P), Φ(C) is a closed set in (Â, d̂). For each n ∈ ℕ, if F_{n} exists then F_{n} is the unique point of C ∩ N_{(n,⟨⟩)}, hence Φ(F_{n}) ∈ Â is the unique point of Φ(C) ∩ Φ(N_{(n,⟨⟩)}). If F_{n} does not exist, then C ∩ N_{(n,⟨⟩)} = ∅, hence Φ(C) ∩ Φ(N_{(n,⟨⟩)}) = ∅. Note also that the sequence of open sets Φ(N_{(n,⟨⟩)}) ⊆ Â, n ∈ ℕ, is arithmetically definable uniformly in n, using the code of Φ^{−1} as a parameter. Thus we can use Π_{1}^{1} comprehension to form the set

S = {n | Φ(C) ∩ Φ(N_{(n,⟨⟩)}) ≠ ∅} = {n | F_{n} exists} = {n | ∃X ψ(n, X)} .

This completes the proof. □

Remark 4. Theorem 1 shows that a certain metrization theorem is logically equivalent to Π_{2}^{1}-CA_{0} over Π_{1}^{1}-CA_{0}. We believe that this is the first convincing instance of a core mathematical theorem which is equivalent to Π_{2}^{1} comprehension, in the sense of reverse mathematics. Previous reverse mathematics results within Z_{2} (see [12, 11]) have involved only set existence axioms which are strictly weaker than Π_{2}^{1} comprehension.^{3}

References

[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 Π_{2}^{1} 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.

3However, Heinatsch and Möllerfeld [2] have shown that Π_{2}^{1}-CA_{0} proves the same Π_{1}^{1} sentences as ACA_{0} plus <ω-Σ_{2}^{0} determinacy, i.e., determinacy for Boolean combinations of G_{δ} sets in the Baire space.

[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.