[FOM] constructive Tychonov

[gcuri@math.unipd.it]

>
> Is there a constructively provable version of the Tychonov product
> theorem?

The Tychonoff product theorem *for topological spaces* is equivalent
to the axiom of choice in ZF, and thus is not provable
constructively (e.g. in constructive or intuitionist ZF, which are
subsystems of ZF).

The constructive failure of this theorem is one of the reasons that
motivate the adoption of a point-free concept of space such as that
of locale or formal space, see

P. T. Johnstone, ``The points of pointless topology'', Bulletin of
the American Mathematical Society, Vol. 8, Number 1, January 1983.


Johnstone's paper

"Tychonoff theorem without the axiom of choice'', Fund. Math. 113
(1981), pp. 21-35.

contains the first choice-free proof of the theorem, but still in a
classical setting (see also Johnstone's  book "Stone Spaces").

As far as I know, the first (choice-free) topos-valid proof of the
localic Tychonoff theorem appeared in J. Vermeulen's Ph.D. thesis
(1986).

The paper

T. Coquand, ``An intuitionistic proof of Tychonoff theorem'', JSL,
vol. 57, n. 1 (1992), pp. 28-32.

went in the direction of proving this result also predicatively, in
Martin-Loef's type theory and Aczel's constructive ZF. However, it
assumed the set indexing the family of formal spaces to have a
decidable equality.

The first fully general and fully constructive and predicative proof
seemingly appeared in:

T. Coquand, ``Compact Spaces and Distributive Lattices''. J. Pure
Appl. Algebra}   184 (2003), no. 1, pp. 1-6.


S. Vickers's paper "Some constructive roads to Tychonoff", recalled
in a previous message, also contains a constructive predicative
proof.

Besides those mentioned here and in the other messages on this
subject, there are also other papers that have dealt with this
result, by Banaschewski,  Johnstone & Vickers...


>And if there is, exactly what does it say, and what
> definition of 'compact' does it use?


The definition of compactness adopted is the usual one using coverings. This is
another reason to consider locales rather than topological spaces: while e.g.
Cantor space or the unit real interval are not compact in the covering sense
(compactness of Cantor space *is* the fan theorem), their point-free
presentations are compact in this sense. This happens precisely because  the
concept of cover is defined without reference to the points.
Independently Martin-Loef and Joyal realized this fact at the end of
the sixties, beginning of the seventies.


Regards,

Giovanni Curi


-----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.

Dipartimento di Matematica Pura ed Applicata
Universita' degli Studi di Padova
www.math.unipd.it