*Steven Vickers*

- Published in print:
- 2005
- Published Online:
- September 2007
- ISBN:
- 9780198566519
- eISBN:
- 9780191713927
- Item type:
- chapter

- Publisher:
- Oxford University Press
- DOI:
- 10.1093/acprof:oso/9780198566519.003.0014
- Subject:
- Mathematics, Logic / Computer Science / Mathematical Philosophy

This chapter discusses the Tychonoff Theorem with respect to point-free topology from the point of view of both topos-valid and predicative mathematics. A new proof of the infinitary Tychonoff ...
More

This chapter discusses the Tychonoff Theorem with respect to point-free topology from the point of view of both topos-valid and predicative mathematics. A new proof of the infinitary Tychonoff Theorem is given using predicative, choice-free methods for possibly undecidable index set. It yields a complete description of the finite basic covers of the product. In contrast to the formal-topological treatment previously given by Negri and Valentini, who followed Coquand's first paper on this subject, the index set of the product under consideration need not be decidable in this chapter's proof. While a more recent approach by Coquand is based on the assumption that each locale under consideration is presented by a distributive lattice of generators, this chapter does not assume the presence of any such presentation. In passing, it highlights the differences and connections between the point-set and the point-free approaches to topology, and between the major varieties of the latter, locale theory, and formal topology.Less

This chapter discusses the Tychonoff Theorem with respect to point-free topology from the point of view of both topos-valid and predicative mathematics. A new proof of the infinitary Tychonoff Theorem is given using predicative, choice-free methods for possibly undecidable index set. It yields a complete description of the finite basic covers of the product. In contrast to the formal-topological treatment previously given by Negri and Valentini, who followed Coquand's first paper on this subject, the index set of the product under consideration need not be decidable in this chapter's proof. While a more recent approach by Coquand is based on the assumption that each locale under consideration is presented by a distributive lattice of generators, this chapter does not assume the presence of any such presentation. In passing, it highlights the differences and connections between the point-set and the point-free approaches to topology, and between the major varieties of the latter, locale theory, and formal topology.