Reverse Mathematics and $\Pi^1_2$ Comprehension

Carl Mummert¹ and Stephen G. Simpson²

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 $\Pi^1_2$ comprehension. An MF space is defined to be a topological space of the form $\MF (P)$ with the topology generated by $\{N_p\mid p\in P\}$. Here $P$ is a poset, $\MF (P)$ is the set of maximal filters on $P$, and $N_p=\{F\in\MF (P)\mid p\in 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 $\mathsf{ACA}_0$ of second order arithmetic. One can prove within $\mathsf{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 $\Pi^1_2$-$\mathsf{CA}_0$. The equivalence is proved in the weaker system $\Pi^1_1$-$\mathsf{CA}_0$. This is the first example of a theorem of core mathematics which is provable in second order arithmetic and implies $\Pi^1_2$ comprehension.

In the foundations of mathematics, there is an ongoing research program known as reverse mathematics. One focuses on specific core mathematical theorems $\tau$, and one determines the weakest set existence axioms which are needed in order to prove $\tau$. Such determinations are made in the context of subsystems of second order arithmetic, $\mathsf{Z}_2$. The strength of $\tau$ is measured by showing that $\tau$ is logically equivalent to a particular subsystem of $\mathsf{Z}_2$, over a weaker subsystem. The standard reference for reverse mathematics and subsystems of $\mathsf{Z}_2$ 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 $\mathsf{Z}_2$ used in this paper are $\mathsf{ACA}_0$, $\Pi^1_1$-$\mathsf{CA}_0$, and $\Pi^1_2$-$\mathsf{CA}_0$. We briefly describe these systems. The language of $\mathsf{Z}_2$ includes number variables $k,m,n,\ldots$ ranging over $\mathbb{N}$, the set of natural numbers, and set variables $X,Y,Z,\ldots$ ranging over subsets of $\mathbb{N}$. All of our systems include first order arithmetic plus the induction axiom

$$\forall X\,[\,(0\in X\land\forall n\,(n\in X\Rightarrow n+1\in X))\Rightarrow \forall n\,(n\in X)\,]\,.$$

The system $\mathsf{ACA}_0$ includes comprehension axioms

$$\exists X\,\forall n\,[\,n\in X\Leftrightarrow \varphi(n)\,]$$

where the formula $\varphi(n)$ does not mention $X$ and is arithmetical, i.e., it contains no set quantifiers. The system $\Pi^1_1$-$\mathsf{CA}_0$ includes comprehension for formulas $\varphi(n)$ which are $\Pi^1_1$, i.e., of the form $\forall Y\,\theta(n,Y)$ where $\theta(n,Y)$ is arithmetical. The system $\Pi^1_2$-$\mathsf{CA}_0$ includes comprehension for formulas $\varphi(n)$ which are $\Pi^1_2$, i.e., of the form $\forall Y\,\exists Z\,\theta(n,Y,Z)$ where $\theta(n,Y,Z)$ is arithmetical. In each of these systems, $\varphi(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 $\mathsf{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 $\mathsf{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 $\mathsf{ACA}_0$.

Definition 2   A poset is a partially ordered set. Within $\mathsf{ACA}_0$, let $P$ be a countable poset. A filter³ on $P$ is a set $F\subseteq P$ such that (1) for all $p\in F$ and $q\ge p$ we have $q\in F$, and (2) for all $p,q\in F$ there exists $r\in F$ such that $p\ge r$ and $q\ge r$. A maximal filter is a filter which is not included in any larger filter. Within $\mathsf{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\in\MF (P)\mid p\in F\}$$

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

Remark 2   In Definition 2 within $\mathsf{ACA}_0$, the countable poset $P$ is regarded as a code for the topological space $\MF (P)$, and each $p\in 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=\bigcup_{p\in L}N_p=\{F\in\MF (P)\mid\exists p\in L\,[\,F\in 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\in N_p$ if and only if $p\in F$, and $F\in U_L$ if and only if $F\cap L\ne\emptyset$. Thus the countable set $L\subseteq P$ may be regarded as a code for the open set $U_L\subseteq\MF (P)$.

Definition 3   Within $\mathsf{ACA}_0$, if $(A,d)$ is a countable pseudometric space, let $(\widehat{A},\widehat{d}\,)$ be the complete separable metric space whose points are the equivalence classes of Cauchy sequences in $(A,d)$, two such sequences $\langle a_n\mid n\in\mathbb{N}\rangle$ and $\langle b_n\mid n\in\mathbb{N}\rangle$ being equivalent if and only if $\lim_nd(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\times\mathbb{Q}^+$$

where $\mathbb{Q}^+$ 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 $\mathsf{ACA}_0$ (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 $(\widehat{A},\widehat{d}\,)$ and the maximal filters on $P_{(A,d)}$. Moreover, a point $x\in\widehat{A}$ belongs to a basic open ball

$$B(a,r)=\left\{x\in\widehat{A}\,\,\big\vert\,\,\widehat{d}(a,x)<r\right\}$$

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 $(\widehat{A},\widehat{d}\,)$ with the countably based MF space $\MF (P)$, where $P=P_{(A,d)}$.

Definition 4   Within $\mathsf{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 $\Phi\subseteq P\times Q$ such that, for all maximal filters $F$ on $P$,

$$\Phi(F)=\{q\in Q\mid\exists p\in F\,[\,(p,q)\in\Phi\,]\,\}$$

is a maximal filter on $Q$. It can be shown that each such code induces a continuous function $\Phi:\MF (P)\to\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 $\Phi:\MF (P)\to\MF (Q)$ together with a coded continuous inverse $\Phi^{-1}:\MF (Q)\to\MF (P)$. The requirement of a coded continuous inverse is apparently not superfluous; we do not know whether it is provable in $\Pi^1_2$-$\mathsf{CA}_0$ that every coded continuous open bijection $\Phi:\MF (P)\to\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 $\mathsf{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 $\mathsf{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_\delta$ set⁴ 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\in U$, there exists an open set $V$ such that $x\in 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 $\Pi^1_2$-$\mathsf{CA}_0$.

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

In the other direction, we prove within $\Pi^1_2$-$\mathsf{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 $\Pi^1_2$-$\mathsf{CA}_0$, let $P$ be a countable poset such that $\MF (P)$ is regular. We use $\Pi^1_2$ comprehension to form the set of ordered pairs $(p,q)\in P\times 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\subseteq\MF (P)$. We use $\Pi^1_2$ comprehension to form the sets

$$\{(a,r,p)\in A\times\mathbb{Q}^+\times P\mid B_1(a,r)\subseteq N_p\}$$

and

$$\{(a,r,p)\in A\times\mathbb{Q}^+\times P\mid N_p\subseteq B_1(a,r)\}$$

where $B_1(a,r)=\{x\in\MF (P)\mid 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 $\mathsf{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 $\mathsf{Z}_2$. We overcome this obstacle by giving a direct proof within $\Pi^1_2$-$\mathsf{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 $\Pi^1_2$ comprehension to construct a homeomorphism between $\MF (P)$ and $(\widehat{A},\widehat{d}_2)=\MF (Q)$ where $Q=P_{(A,d_2)}$. This proves our lemma.$\Box$

Theorem 1   The following are equivalent over $\Pi^1_1$-$\mathsf{CA}_0$.

1. $\Pi^1_2$ comprehension.
2. MFMT.

Proof.Lemma 1 shows that $\Pi^1_2$ comprehension implies MFMT. It remains to prove the reversal. We work in $\Pi^1_1$-$\mathsf{CA}_0$ and assume MFMT. Consider a $\Sigma^1_2$ formula $\exists X\,\psi(n,X)$ where $\psi(n,X)$ is $\Pi^1_1$. In order to prove $\Pi^1_2$ comprehension, it suffices to prove the existence of the set $S=\{n\in\mathbb{N}\mid\exists X\,\psi(n,X)\}$. By Kondo's $\Pi^1_1$ uniformization theorem (provable in $\Pi^1_1$-$\mathsf{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 $\psi(n,X)$ holds.

We write $\psi(n,X)$ in normal form as $\lnot\exists f\,\forall m\,R(n,X[m],f[m])$. Here we are using the finite sequence notation $X[m]=\langle X(0),\ldots,X(m-1)\rangle$ and $f[m]=\langle f(0),\ldots,f(m-1)\rangle$. We may safely assume that $\forall n\,R(n,\langle\rangle,\langle\rangle)$ holds. For finite sequences $\sigma$ and $\tau$, we write $\sigma\supset\tau$ if and only if $\tau$ is a proper initial segment of $\sigma$. Let $P$ be the countable poset consisting of all ordered triples $(n,X[k],f[k])$ such that $(\forall m\le 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]\supset X'[k']$ and $f[k]\supset f'[k']$.
2. $(n,X[k])<(n',X'[k'])$ if and only if $n=n'$ and $X[k]\supset X'[k']$.
3. $(n,X[k],f[k])<(n',X'[k'])$ if and only if $n=n'$ and $X[k]\supset 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\in P\mid q\le p\}$ where $q$ is a minimal element of $P$.
2. $F=\{(n,X[k],f[k]),(n,X[k])\mid k\in\mathbb{N}\}$ where $n,X,f$ are such that $\forall m\,R(n,X[m],f[m])$ holds.
3. $F=F_n=\{(n,X_n[k])\mid k\in\mathbb{N}\}$ where $n$ is such that $\exists X\,\psi(n,X)$.

Note that there is a closed set $C\subseteq\MF (P)$ consisting of $F_n$ for all $n$ such that $\exists X\,\psi(n,X)$ holds. The complement of $C$ is the open set $\bigcup_{n\in\mathbb{N}}N_{(n,\langle\rangle,\langle\rangle)}$.

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\in N_p$, we can find a basic open set $N_q$ such that $F\in 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\in P\mid q\le 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=\bigcup_{q\in M}N_q$$

where $M$ is the set of minimal elements of $P$.

Case 2: $F=\{(n,X[k],f[k]),(n,X[k])\mid k\in\mathbb{N}\}$ where $n,X,f$ are such that $\forall m\,R(n,X[m],f[m])$ holds. It follows that $\psi(n,X)$ fails. Hence $X\ne X_n$ if $X_n$ exists. Suppose $F\in N_p$, i.e., $p\in F$. If $p=(n,X[k])$, then $N_p$ is closed, because the complement of $N_p$ is the open set

$$(W\setminus N_p)\cup\bigcup_{p'\in L'}N_{p'}$$

where $L'$ is the set of $p'=(n',X'[k])\in P$ such that $n'\ne n$ or $X'[k]\ne X[k]$. If $p=(n,X[k],f[k])$, let $m\ge k$ be so large that $X[m]\ne X_n[m]$ if $X_n$ exists, and put $q=(n,X[m],f[m])$. Then $F\in N_q\subseteq N_p$. Moreover, $N_q$ is closed, because the complement of $N_q$ is the open set

$$(W\setminus N_q)\cup\bigcup_{p'\in L''}N_{p'}\cup\bigcup_{q'\in M''}N_{q'}$$

where $L''$ is the set of $p'=(n',X'[m])$ such that $n'\ne n$ or $X'[m]\ne X[m]$, and $M''$ is the set of $q'=(n',X'[m],f'[m])\in P$ such that $n'\ne n$ or $X'[m]\ne X[m]$ or $f'[m]\ne f[m]$.

Case 3: $F=F_n$. In this case, for all $N_p$ such that $F\in 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 $\Phi$ of $\MF (P)$ onto a complete separable metric space $(\widehat{A},\widehat{d}\,)$. In particular, since $C$ is a closed set in $\MF (P)$, $\Phi(C)$ is a closed set in $(\widehat{A},\widehat{d}\,)$. For each $n\in\mathbb{N}$, if $F_n$ exists then $F_n$ is the unique point of $C\cap N_{(n,\langle\rangle)}$, hence $\Phi(F_n)\in\widehat{A}$ is the unique point of $\Phi(C)\cap\Phi(N_{(n,\langle\rangle)})$. If $F_n$ does not exist, then $C\cap N_{(n,\langle\rangle)}=\emptyset$, hence $\Phi(C)\cap\Phi(N_{(n,\langle\rangle)})=\emptyset$. Note also that the sequence of open sets $\Phi(N_{(n,\langle\rangle)})\subseteq\widehat{A}$, $n\in\mathbb{N}$, is arithmetically definable uniformly in $n$, using the code of $\Phi^{-1}$ as a parameter. Thus we can use $\Pi^1_1$ comprehension to form the set

$$S=\{n\mid\Phi(C)\cap\Phi(N_{(n,\langle\rangle)})\ne\emptyse... ...\{n\mid F_n\hbox{ exists}\}=\{n\mid\exists X\,\psi(n,X)\}\,.$$

This completes the proof. $\Box$

Remark 4   Theorem 1 shows that a certain metrization theorem is logically equivalent to $\Pi^1_2$-$\mathsf{CA}_0$ over $\Pi^1_1$-$\mathsf{CA}_0$. We believe that this is the first convincing instance of a core mathematical theorem which is equivalent to $\Pi^1_2$ comprehension, in the sense of reverse mathematics. Previous reverse mathematics results within $\mathsf{Z}_2$ (see [12,11]) have involved only set existence axioms which are strictly weaker than $\Pi^1_2$ comprehension.⁵

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 $\Pi^1_2$ 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.

About this document ...

Reverse Mathematics and $\Pi^1_2$ 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

... Mummert¹

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²

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.

...filter³

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⁴

In the context of arbitrary topological spaces, a $G_\delta$ 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_\delta$ 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 $\Pi^1_1$ set which is not boldface $\Sigma^1_1$. See also [8, proof of Theorem 2.3.40] and [9].

... comprehension.⁵

However, Heinatsch and Möllerfeld [2] have shown that $\Pi^1_2$-$\mathsf{CA}_0$ proves the same $\Pi^1_1$ sentences as $\mathsf{ACA}_0$ plus ${<}\omega$-$\Sigma^0_2$ determinacy, i.e., determinacy for Boolean combinations of $G_\delta$ sets in the Baire space.