From mboxrd@z Thu Jan 1 00:00:00 1970
X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/47
Path: news.gmane.org!not-for-mail
From: "Prof. Peter Johnstone"
Newsgroups: gmane.science.mathematics.categories
Subject: Re: "Kantor dust"
Date: Sat, 7 Feb 2009 17:18:29 +0000 (GMT)
Message-ID:
Reply-To: "Prof. Peter Johnstone"
NNTP-Posting-Host: lo.gmane.org
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
X-Trace: ger.gmane.org 1234039421 24723 80.91.229.12 (7 Feb 2009 20:43:41 GMT)
X-Complaints-To: usenet@ger.gmane.org
NNTP-Posting-Date: Sat, 7 Feb 2009 20:43:41 +0000 (UTC)
To: Vaughan Pratt , categories list
Original-X-From: categories@mta.ca Sat Feb 07 21:44:56 2009
Return-path:
Envelope-to: gsmc-categories@m.gmane.org
Original-Received: from mailserv.mta.ca ([138.73.1.1])
by lo.gmane.org with esmtp (Exim 4.50)
id 1LVu2p-0007Hl-RJ
for gsmc-categories@m.gmane.org; Sat, 07 Feb 2009 21:44:55 +0100
Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1LVtPW-00034X-7B
for categories-list@mta.ca; Sat, 07 Feb 2009 16:04:18 -0400
Original-Sender: categories@mta.ca
Precedence: bulk
Xref: news.gmane.org gmane.science.mathematics.categories:47
Archived-At:
On Fri, 6 Feb 2009, Vaughan Pratt wrote:
>
> Toby Bartels wrote:
>> But it's not a constructive theorem that every such x has a binary
>> expansion.
>> That's still a neat result, that the binary reals are given by N^N,
>> but the binary reals aren't constructively the same as the reals.
>
> Whose reals, Cauchy's or Dedekind's?
Toby was of course referring to the Dedekind reals, but your binary
reals are not constructively either the Cantor or the Dedekind reals.
The reason is that you have to know in advance that a binary
sequence isn't going to end in an infinite string of 1's; by excluding
those sequences, you make the question "Is x < 1/2?" decidable,
which is not constructively true of either the Cantor reals or the
Dedekind reals.
> If the latter then that's no
> surprise---carrying out constructions with open order filters is less
> constructive than with the Cauchy sequence concept. Lubarsky and
> Rathien in Logic and Analysis 1:2 131-152 have recently made the point
> that whereas Cauchy reals can be understood constructively as a set, any
> attempt to make Dedekind's reals constructive turns them into a proper
> class.
>
> Between Dedekind cuts and Cauchy sequences, the more appropriate notion
> of reals for constructive analysis would surely be the Cauchy reals.
I could take issue with you on this. If you insist that "constructive"
entails "predicative", then you are of course right; but in a topos-
theoretic context, where you don't have countable choice automatically
available, it's very much the other way round.
>>
>> In the topos of sheaves on the real line,
>> every function from [0,1) to N is constant,
>> yet there are obviously many other functions from N^N to N.
>> Thus N^N and [0,1) are not constructively isomorphic as sets,
>> so there is no way to give N^N the order type of [0,1) constructively.
>
> Let's compare apples with apples here. There are presumably going to be
> nonconstant *functions* from the Freyd coalgebra object to 2 in this
> topos, although they won't be continuous with respect to the topology
> induced on that object by its coalgebra structure.
No -- that's the whole point. In the topos of sheaves on R (better, in
the gros topos of sheaves on topological spaces) every function
R --> R is continuous, hence every function [0,1] --> 2 is constant.
Peter Johnstone