From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2595 Path: news.gmane.org!not-for-mail From: Steve Vickers Newsgroups: gmane.science.mathematics.categories Subject: Re: mystification and categorification Date: Mon, 08 Mar 2004 10:20:23 +0000 Message-ID: References: <200403060649.i266nuaG014947@coraki.Stanford.EDU> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241018768 4908 80.91.229.2 (29 Apr 2009 15:26:08 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:26:08 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Mon Mar 8 16:50:15 2004 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 08 Mar 2004 16:50:15 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 1B0RgU-0000OL-00 for categories-list@mta.ca; Mon, 08 Mar 2004 16:49:11 -0400 User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.3) Gecko/20030312 X-Accept-Language: en-us, en In-Reply-To: <200403060649.i266nuaG014947@coraki.Stanford.EDU> Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 16 Original-Lines: 38 Xref: news.gmane.org gmane.science.mathematics.categories:2595 Archived-At: 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.