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.