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.