# [FOM] constructive Tychonov

Stephen G Simpson simpson at math.psu.edu
Thu Nov 29 11:38:49 EST 2007

```Robert Black wrote:
> Is there a constructively provable version of the Tychonov product
> theorem? And if there is, exactly what does it say, and what
> definition of 'compact' does it use?

Perhaps the simplest constructively provable version of Tychonoff's
Theorem is as follows.

The product of a sequence of totally bounded (complete) metric
spaces is totally bounded (and complete).

In more detail:

Suppose we have a sequence of (complete) metric spaces X[n] and a
double sequence of finite sets F[m,n] in X[n] such that for all x in
X[n] we can find y in F[m,n] such that d(x,y) < 1/m .  Let X be the
product of the X[n]'s with the usual (complete) product metric.
Then, we can find a sequence of finite sets F[m] in X such that for
all m and all x in X we can find y in F[m] such that d(x,y) < 1/m.

This is not only constructively provable but also provable in, for
instance, RCA_0.  This fact is very useful in the development of
analysis in RCA_0 and other weak subsystems of second-order
arithmetic.  See my book Subsystems of Second Order Arithmetic.

-- Steve

Name: Stephen G. Simpson

Affiliation: Professor of Mathematics, Pennsylvania State University

Research Interests: mathematial logic, foundations of mathematics

Web page: http://www.math.psu.edu/simpson/.

```