[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.
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/.
More information about the FOM