Many fundamental results as the theorems of Tychonoff and Hahn-Banach are equivalent, in classical ZF, to some form of choice principle. A well-known advantage of replacing topological spaces with locales, or formal spaces, is that topos-valid (choice-free) versions of these results become often provable. Generally speaking, this remains true even if one replaces topoi with constructive (intuitionistic and predicative) settings such as Type Theory or Constructive Set Theory. This paper deals with the rather extreme case of Stone-Čech compactification ß. The formal spaces/ locales X for which ß(X) exists constructively are characterized. This involves discussing the 'size' of hom-sets in the category Loc of locales/formal spaces (constructively Loc is not locally small). In particular, the full subcategory of locally compact regular locales is proved to be locally small. It is also shown how Stone-Čech compactification can itself be used to prove that certain hom-sets are small.

Exact approximations to Stone-Čech compactification.

CURI, Giovanni
2007-01-01

Abstract

Many fundamental results as the theorems of Tychonoff and Hahn-Banach are equivalent, in classical ZF, to some form of choice principle. A well-known advantage of replacing topological spaces with locales, or formal spaces, is that topos-valid (choice-free) versions of these results become often provable. Generally speaking, this remains true even if one replaces topoi with constructive (intuitionistic and predicative) settings such as Type Theory or Constructive Set Theory. This paper deals with the rather extreme case of Stone-Čech compactification ß. The formal spaces/ locales X for which ß(X) exists constructively are characterized. This involves discussing the 'size' of hom-sets in the category Loc of locales/formal spaces (constructively Loc is not locally small). In particular, the full subcategory of locally compact regular locales is proved to be locally small. It is also shown how Stone-Čech compactification can itself be used to prove that certain hom-sets are small.
2007
Stone-Čech compactification; locales; formal spaces; axiom of choice; toposes; constructive set theories.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/324101
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact