Prof. Peter Johnstone wrote:
Dear Thomas,
I'm pretty sure that what Michael meant by "separable" was what most topologists would call "second countable" -- i.e., countably generated as a frame. (There are some topology textbooks in which this condition is called "completely separable".)
Peter Johnstone --------------------------------- On Tue, 30 Jun 2009, Thomas Streicher wrote:
Recently rereading Fourman's "Continuous Truth" I came across the term "separable locale" but could nowhere find an explanation. Does it mean a cHa A for which there exists a countable subset B such that ever a in A is the supremum of those b in B with b leq a. This would be the point free account of "second countable", i.e. having a countable basis. Of course, second countable T_) spaces are separable, i.e. have a countable dense set. Is this reading the "usual" one?
Thomas
Thomas, Peter is correct about my intention. More precisely, 'separable' is defined in Formal Spaces (FS) (Fourman & Grayson, Brouwer Centenary Symposium) 3.12(c) --- although I now find this account unnecessarily obscure. What you say below is correct classically; constructively there is some subtlety. A locale is separable iff it is presented (as in FS 1.1) by a countable language with decidable \leq and countably many *inhabited* basic covers. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]