# Summary

Tychonoff's theorem in the framework
of formal topologies , by S. Negri and S. Valentini,
**The Journal of Symbolic Logic**, 62,4, pp. 1315-1332, 1997.
negri@helsinki.fi

##

(From the introduction)
"In this paper we give a constructive proof of the pointfree version of
Tychonoff's theorem
within formal topology, using ideas from Coquand's proof in \cite{C}.
To deal with pointfree topology Coquand uses Johnstone's coverages.
Because of the representation theorem in \cite{BS}, from a
mathematical viewpoint these structures
are equivalent to formal topologies but there is an essential
difference also. Namely,
formal topologies have been developed within Martin L\"of's
constructive type theory (cf. \cite{ML}), which thus gives a direct
way of formalizing them (cf. \cite{JC}).
The most important aspect of our proof is that it is based on
an inductive definition
of the topological product of formal topologies. This fact allows us
to transform Coquand's proof into a proof by structural induction on
the last rule applied in a derivation of a cover. The inductive
generation of a cover, together with a modification of the inductive
property proposed by Coquand, makes it possible to formulate our
proof of Tychonoff's theorem in constructive type theory. There is
thus a clear difference to earlier localic proofs of Tychonoff's
theorem known in the literature (cf. \cite{J}, \cite{J1}, \cite{JV},
\cite{Kr}).
Indeed we not only avoid to use the axiom of choice, but reach
constructiveness in a
very strong sense. Namely, our proof of Tychonoff's theorem supplies
an algorithm
which, given a cover of the product space, computes a finite
subcover, provided that
there exists a similar algorithm for each component space. Since type
theory has been
implemented on a computer (cf. \cite{NPS}), an eventual strict
formalization of our
proof will at the same time be a computer program that executes the
task of finding
a finite subcover.
The paper is organized as follows. In the first part we recall the
basic definitions and motivations of formal topologies and introduce
in this framework
the notion of topological product. Tychonoff's theorem is then proved
both for the
binary and arbitrary product of topological spaces. Next we relate
our proof to the proof of Johnstone and Vickers (cf. \cite{JV}). In
an appendix, it is shown how to define the type ${\cal
P}_{\omega}(S)$ of finite subsets of the type $S$ and the type
$\Pi_{\omega}(I,B)$ of finite support functions from $I$ to the
indexed family of sets $B(i)$, where $i\in I$. In a second appendix,
the formal definition of the coproduct of formal topologies is
detailed."
Back to Sara's homepage.