[FOM] Question for Nik Weaver

[Andrej Bauer]

On Thursday 23 February 2006 06:01, Bill Taylor wrote:
> Nik, you made this comment in an article yesterday...
>
> > it is possible to treat things like
> > the real line and the power set of N essentially as proper classes
>
> Presumably this apposition implies that you do NOT think of P(N) and R
> as being essentially isomorphic? (OC one should remove the finite sets
> from P(N) to do this most conveniently.)

For examples of such treatments see Formal Topology (a predicative and 
constructive treatment of topology), where a space might be (usually is) a 
proper class, and the reals are not the same thing as the class of predicates 
on N. I do not know off the top of my head what the best reference for this 
would be, but certainly you should look at work by Giovanni Sambin and 
coworkers, as well as work of Peter Aczel. At least one of them is on this 
list. Perhaps we can induce him to explain why spaces are classes and not 
sets in Formal Topology. Is this just a limitation of the formal framework 
they work in, or is there a mathematical idea behind such treatment?

Andrej Bauer