[FOM] constructive Tychonov

[Stephen G Simpson]

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