[FOM] Tychonoff and Choice

[Andreas Blass]

Harvey Friedman wrote:

> It is provable in ZF that the product of any countably infinite 
> sequence of
> two point spaces (each with the discrete topology) is compact.
>
> It is not provable in ZF that the product of any countably infinite
> sequence of three point spaces (each with the discrete topology) is
> compact.

Andrej Bauer objected:

> Both claims cannot hold, since {0,1}^omega and {0,1,2}^omega are 
> obviously
> homeomorphic, therefore they are either both compact or both 
> non-compact.

But Harvey is right.  His statement was not about {0,1}^omega and 
{0,1,2}^omega but about the product of a countably infinite sequence of 
two (or three) point spaces.  The "obvious" homeomorphism between such 
a product and {0,1}^omega (or {0,1,2}^omega) depends on the axiom of 
choice --- you have to choose, for each factor in the product, a 
bijection to {0,1} (or to {0,1,2}).  Both {0,1}^omega and {0,1,2}^omega 
are compact, but that doesn't help in the case of a product of 
countably many arbitrary three point spaces.  By the way, Harvey's 
first result (compactness when the factors have two points) looks to me 
like a nice application of the law of the excluded middle.  Either the 
product is empty, in which case it's trivially compact, or it has an 
element, from which one can easily define a bijection to {0,1}^omega.

Andreas Blass