Re: mystification and categorification

[Steve Vickers <s.j.vickers@cs.bham.ac.uk>]

Vaughan Pratt wrote:

>(The power set of a set is a Boolean algebra,
>for heaven's sake.  Why on earth forget that structure prior to taking the
>second exponentiation?  Set theorists seem to think that they can simply
>forget structure without paying for it, but in the real world it costs
>kT/2 joules per element of X to forget that structure.  If set theorists
>aren't willing to pay real-world prices in their modeling, why should we
>taxpayers pay them real-world salaries?  Large cardinals are a figment of
>their overactive imaginations, and the solution to consistency concerns is
>not to go there.)
>
>Vaughan Pratt
>

Dear Vaughan,

I like it!

But there's still the question of just what structure the power set has.
Constructively it's not a Boolean algebra in general, though it is a frame.

And is it even a set? You can in fact only say that by removing the
structure, which is exactly what you told the set-theorists not to do.
And in this instance it's arguable. Topos theorists say it is a set,
predicative type theorists say it isn't.

Part of the structure of the power "set" is topological - the Scott
topology, with the inclusion order as its specialization order. But to
formalize it as topological space, point-set + topological structure,
you again have to forget structure in order to get a point-set. Taking
this seriously generally brings you to point-free topology in some form
or other.

Steve Vickers.