Formal spaces. (English) Zbl 0537.03040

The L. E. J. Brouwer Centen. Symp., Proc. Conf., Noordwijkerhout/Holl. 1981, Stud. Logic Found. Math. 110, 107-122 (1982).
[For the entire collection see Zbl 0505.00008.]
This paper is an introduction to the constructive theory of locales (or ’pointless spaces’) from the point of view of intuitionistic propositional theories. It is shown how such a theory gives rise to a ’Lindenbaum algebra’ which is the dual of a locale (called the formal space of the theory), and how properties of the theory are reflected in properties of its formal space. In particular, the question of whether the formal space really is a space (i.e. whether it has enough points) becomes the question of whether the theory is complete (i.e. has enough models), and some well-known examples of this phenomenon are discussed. \(\{\) The paper is marred by an unfortunate wrong definition: for a map of locales \(f:\quad X\to Y\) to be open, it is not sufficient (unless Y is the one-point space) merely for \(f^*\) to have a left adjoint. Thus the result (ascribed to A. Joyal in Lemma 4.5) that a locally compact locale embeds as an open sublocale of its Stone space is false, even for stably locally compact locales. The correct definition of openness may be found in a paper by A. Joyal and M. Tierney [An extension of the Galois theory of Grothendieck, Mem. Am. Math. Soc. (to appear)].\(\}\)
Reviewer: P.T.Johnstone


03F55 Intuitionistic mathematics
03C90 Nonclassical models (Boolean-valued, sheaf, etc.)
03G30 Categorical logic, topoi
54A05 Topological spaces and generalizations (closure spaces, etc.)


Zbl 0505.00008