From MAILER-DAEMON Wed Mar 4 17:51:35 2009 Date: 04 Mar 2009 17:51:35 -0400 From: Mail System Internal Data Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA Message-ID: <1236203495@mta.ca> X-IMAP: 1233509219 0000000078 Status: RO This text is part of the internal format of your mail folder, and is not a real message. It is created automatically by the mail system software. If deleted, important folder data will be lost, and it will be re-created with the data reset to initial values. From rrosebru@mta.ca Sun Feb 1 13:24:58 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 01 Feb 2009 13:24:58 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LTg2y-0005xO-Ox for categories-list@mta.ca; Sun, 01 Feb 2009 13:23:52 -0400 Mime-Version: 1.0 (Apple Message framework v624) Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit From: Paul Taylor Subject: categories: Kantor dust Date: Sun, 1 Feb 2009 16:14:33 +0000 To: Categories list Sender: categories@mta.ca Precedence: bulk Reply-To: Paul Taylor Message-Id: Status: O X-Status: X-Keywords: X-UID: 1 There are some significant mathematical points that can be made in response to Vasili Galchin's question about the "constructive" existence of Cantor space, but I fear that these are going to get lost in the cross-fire of comments that neither state their background assumptions nor lay out the mathematics. It is well over a century since we discovered that it is meaningless to talk about the absolute truth or falsity of (semantical) statements in mathematics. There are many many people and foundational positions that call themselves "constructive". Unfortunately the experts in these theories have a tendency to assert a monopoly on the word, and ignore the existence of the other points of view, whilst non-experts repeat half-remembered and mis-understood opinions that may originate from the opponents and not the proponents of the theories. On the other hand, Peter Schuster and Giovanni Sambin have made some effort in recent years to bring these disciplines together. I am not going to attempt to make a list of "constructive" theories, and I would strongly advise against referring to such lists elsewhere, ESPECIALLY in Wikipedia. Nor am I going to try to represent positions other than my own -- I invite the respective experts to do this. Traditionally, Cantor space is described as a subspace of R or [0,1] using the "middle third" construction, but I learned it like that long before I became a constructivist of any kind, so I don't know whether there are any constructive subtleties associated with this view. I think of Cantor as the exponential 2^N, so FOR EXAMPLE it makes sense to talk about it in any CCC, or a topos. However, the interesting question is what it looks like as a TOPOLOGICAL SPACE, in the many different interpretations of that phrase. We can do topology starting from the points, or starting from the open sets. In the latter case, these have a basis whose members are named by FINITE sets of integers: a point of Cantor space is a decidable (possibly) infinite set of integers, and lies in a basic open set if the infinite set includes the finite one. The first interesting mathematical question is this: if we define Cantor space starting from its points, but take these to be given by TOTAL RECURSIVE FUNCTIONS N-->2, and then put the topology that I have just mentioned on it, what are the properties of this topology? In particular, is it compact? The answer is no, because of the "Kleene Tree". This is a computably defined infnite tree that has no infinite computable path. There are many descriptions of this, including one by Andrej Bauer: math.andrej.com/2006/04/25/konigs-lemma-and-the-kleene-tree/ The second interesting mathematical point is that, by looking at the open sets instead of the points as our formulation of topology, the answer is different. The whole of this discussion can be conducted using the closed real interval in place of Cantor space, so many things are better documented in the literature for one example rather than the other. In particular, compactness of the interval has more careful descriptions in: LOCALE THEORY: Michael Fourman and Martin Hyland, "Sheaf models for analysis", in Michael Fourman, Chris Mulvey, and Dana Scott, editors, "Applications of Sheaves", number 753 in Lecture Notes in Mathematics, pages 280--301. Springer-Verlag, 1979. FORMAL TOPOLOGY: Jan Cederquist and Sara Negri, "A constructive proof of the Heine--Borel covering theorem for formal reals", in Stefano Beradi and Mario Coppo, editors, "Types for Proofs and Programs", number 1158 in Lecture Notes in Computer Science, page 6275. Springer-Verlag, 1996. ABSTRACT STONE DUALITY: Andrej Bauer and Paul Taylor, "The Dedekind reals in abstract Stone duality", www.PaulTaylor.EU/ASD/dedras I wrote a sketch (not a properly written paper) about the construction of Cantor Space in ASD and its compactness in "Tychonov's Theorem in ASD", www.PaulTaylor.EU/ASD/misclc.php#tyctas Paul Taylor PS Please refer to my website as paultaylor.eu, not monad.me.uk, as it will be moving home shortly, and I will be better able to ensure continuity of service for the name paultaylor.eu, whilst I would like to discontinue monad.me.uk at some stage. From rrosebru@mta.ca Sun Feb 1 19:29:23 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 01 Feb 2009 19:29:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LTlk6-0001eI-Aw for categories-list@mta.ca; Sun, 01 Feb 2009 19:28:46 -0400 Date: Sun, 1 Feb 2009 18:53:52 +0000 (GMT) From: "Prof. Peter Johnstone" To: Vaughan Pratt , categories list Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Prof. Peter Johnstone" Message-Id: Status: O X-Status: X-Keywords: X-UID: 2 On Sat, 31 Jan 2009, Vaughan Pratt wrote: > I'm not aware of any reason why a topos with a Cantor set object K has > to also have a natural number object N, though I'm not enough of a topos > hacker myself to know how to produce one with K but without N (but would > be happy to learn). Does such a topos exist in nature? And what can be > said of the free topos with Cantor set object? > A topos with a Cantor set object (i.e. a final coalgebra for FX = X+X) necessarily has a natural number object. Observe that the Cantor set K necessarily has a point (since 1 has an F-coalgebra structure), so the isomorphism K+K \cong K yields a monomorphism K \to K and a point disjoint from its image. From there on, use Corollary D5.1.3 in the Elephant. Peter Johnstone From rrosebru@mta.ca Sun Feb 1 19:29:23 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 01 Feb 2009 19:29:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LTljM-0001bb-Oc for categories-list@mta.ca; Sun, 01 Feb 2009 19:28:00 -0400 Date: Sun, 1 Feb 2009 19:18:33 +0100 From: gcuri@math.unipd.it To: categories@mta.ca Subject: categories: Re: Kantor dust MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: gcuri@math.unipd.it Message-Id: Status: O X-Status: X-Keywords: X-UID: 3 Further references on the constructive presentation of Cantor space are: 1. P. Martin-Lof, Notes on Constructive Mathematics. Almqvist and Wiksel= l, 1970. 2. M. Fourman, R. Grayson, Formal Spaces. In: The L.E.J. Brouwer Centenar= y Symposium, A.S. Troelstra and D. van Dalen, eds. North Holland, 1982, pp= . 107-122. Compactness of Cantor space is equivalent to the fan theorem which is equ= ivalent to spatiality of formal Cantor space (Cantor locale). Best regards, Giovanni Curi Quoting Paul Taylor : > There are some significant mathematical points that can be made in > response to Vasili Galchin's question about the "constructive" > existence of Cantor space, but I fear that these are going to get > lost in the cross-fire of comments that neither state their background > assumptions nor lay out the mathematics. It is well over a century > since we discovered that it is meaningless to talk about the absolute > truth or falsity of (semantical) statements in mathematics. > > There are many many people and foundational positions that call > themselves "constructive". Unfortunately the experts in these > theories have a tendency to assert a monopoly on the word, and ignore > the existence of the other points of view, whilst non-experts > repeat half-remembered and mis-understood opinions that may originate > from the opponents and not the proponents of the theories. On the > other hand, Peter Schuster and Giovanni Sambin have made some effort > in recent years to bring these disciplines together. > > I am not going to attempt to make a list of "constructive" theories, > and I would strongly advise against referring to such lists elsewhere, > ESPECIALLY in Wikipedia. Nor am I going to try to represent positions > other than my own -- I invite the respective experts to do this. > > Traditionally, Cantor space is described as a subspace of R or [0,1] > using the "middle third" construction, but I learned it like that > long before I became a constructivist of any kind, so I don't know > whether there are any constructive subtleties associated with this view= . > > I think of Cantor as the exponential 2^N, so FOR EXAMPLE it makes > sense to talk about it in any CCC, or a topos. However, the > interesting question is what it looks like as a TOPOLOGICAL SPACE, > in the many different interpretations of that phrase. > > We can do topology starting from the points, or starting from the > open sets. In the latter case, these have a basis whose members are > named by FINITE sets of integers: a point of Cantor space is a > decidable (possibly) infinite set of integers, and lies in a basic > open set if the infinite set includes the finite one. > > The first interesting mathematical question is this: if we define > Cantor space starting from its points, but take these to be given > by TOTAL RECURSIVE FUNCTIONS N-->2, and then put the topology > that I have just mentioned on it, what are the properties of this > topology? In particular, is it compact? > > The answer is no, because of the "Kleene Tree". This is a computably > defined infnite tree that has no infinite computable path. There > are many descriptions of this, including one by Andrej Bauer: > math.andrej.com/2006/04/25/konigs-lemma-and-the-kleene-tree/ > > The second interesting mathematical point is that, by looking at the > open sets instead of the points as our formulation of topology, the > answer is different. > > The whole of this discussion can be conducted using the closed real > interval in place of Cantor space, so many things are better > documented in the literature for one example rather than the other. > In particular, compactness of the interval has more careful > descriptions in: > > LOCALE THEORY: Michael Fourman and Martin Hyland, "Sheaf models for > analysis", in Michael Fourman, Chris Mulvey, and Dana Scott, editors, > "Applications of Sheaves", number 753 in Lecture Notes in Mathematics= , > pages 280--301. Springer-Verlag, 1979. > > FORMAL TOPOLOGY: Jan Cederquist and Sara Negri, "A constructive proof > of the Heine--Borel covering theorem for formal reals", in > Stefano Beradi and Mario Coppo, editors, "Types for Proofs and > Programs", number 1158 in Lecture Notes in Computer Science, > page 6275. Springer-Verlag, 1996. > > ABSTRACT STONE DUALITY: Andrej Bauer and Paul Taylor, "The Dedekind > reals in abstract Stone duality", www.PaulTaylor.EU/ASD/dedras > > I wrote a sketch (not a properly written paper) about the construction > of Cantor Space in ASD and its compactness in "Tychonov's Theorem in > ASD", > www.PaulTaylor.EU/ASD/misclc.php#tyctas > > Paul Taylor > > PS Please refer to my website as paultaylor.eu, not monad.me.uk, as > it will be moving home shortly, and I will be better able to ensure > continuity of service for the name paultaylor.eu, whilst I would like > to discontinue monad.me.uk at some stage. > > > > > > > ----------------------------------------------------------------- This message was sent using IMP, the Internet Messaging Program. Dipartimento di Matematica Pura ed Applicata Universita' degli Studi di Padova www.math.unipd.it From rrosebru@mta.ca Sun Feb 1 19:30:14 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 01 Feb 2009 19:30:14 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LTllR-0001i6-Pf for categories-list@mta.ca; Sun, 01 Feb 2009 19:30:09 -0400 MIME-Version: 1.0 Date: Sun, 1 Feb 2009 20:11:25 +0100 Subject: categories: Question on "On Closed Categories of Functors" From: Tony Meman To: categories Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Tony Meman Message-Id: Status: O X-Status: X-Keywords: X-UID: 4 Dear category theorists, I have a question concerning the paper "On Closed Categories of Functors" from Brian Day (By the way, this is an excellent paper). Let V be a symmetric monoidal closed category and C a small V-category. The (ordinary) category [C,V] of V-functors admits the sturcure of a V-category in a canonical way. A symmetric monoidal V-category is the enriched analogue of a symmetric-monoidal structure on an ordinary category, i.e. all the structure morphisms are V-morphisms and the coherence conditions are fullfilled. The underlaying category of a symmetric monoidal V-category admits the structure of an ordinary symmetric monoidal category. Brian Day constructs a symmetric monoidal closed structure ([C,V],@,E) on the V-category of V-functors [C,V] for some cases [3.3, 3.6], e.g. if (C,*,e) is a symmetric monoidal V-category [4.1]. The underlaying *category* [C,V] of V-functors admits a closed symmetric monoidal structure from the enriched one by taking the underlaying functor of each V-functor, the underlaying natural transformation of each V-natural transformation. Because a closed symmetric monoidal category is canonically enriched over itself, the category [C,V] gets a [C,V] enrichment in this way. My question is: What does this [C,V]-enrichment of [C,V] have to do with the V-enrichment of [C,V]? Suppose C have a terminal object t. One gets a evaluation functor Ev_t:[C,V]-CAT-->V-CAT. Is this the connection between the two enrichments? Thank you in advance for any help. Tony From rrosebru@mta.ca Mon Feb 2 17:33:39 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 02 Feb 2009 17:33:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LU6NX-0000v6-1t for categories-list@mta.ca; Mon, 02 Feb 2009 17:30:51 -0400 Date: Sun, 01 Feb 2009 17:16:16 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: Kantor dust Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 5 Paul Taylor wrote: > The first interesting mathematical question is this: if we define > Cantor space starting from its points, but take these to be given > by TOTAL RECURSIVE FUNCTIONS N-->2, and then put the topology > that I have just mentioned on it, what are the properties of this > topology? In particular, is it compact? > > The answer is no, because of the "Kleene Tree". This is a computably > defined infnite tree that has no infinite computable path. There > are many descriptions of this, including one by Andrej Bauer: > math.andrej.com/2006/04/25/konigs-lemma-and-the-kleene-tree/ > [...] > ABSTRACT STONE DUALITY: Andrej Bauer and Paul Taylor, "The Dedekind > reals in abstract Stone duality", www.PaulTaylor.EU/ASD/dedras In concrete Stone duality, increasing structure on one side is offset by decreasing structure on the other. One would hope for a similar phenomenon in abstract Stone duality. If we can consider constructivity as part of the structure of an object, then we should expect that the more constructive some type of object, the less constructive the "object of all objects of that type." So for example if (total) recursive functions are demonstrably more constructive than partial recursive functions by some criterion, we should expect the set of all recursive functions to be *less* constructive than that of partial recursive functions by the same criterion, rather than more. The phenomena you're observing here seem entirely consistent with this principle, and point up the need to be clear, when judging constructivity in some context, whether it is the collection or the individuals therein being so judged, with the added complication that Stone duality makes the roles of collection and individual therein interchangeable, such as when elements of sets are understood as ultrafilters of Boolean algebras. Vaughan Pratt From rrosebru@mta.ca Mon Feb 2 17:33:39 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 02 Feb 2009 17:33:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LU6OH-0000zG-Ju for categories-list@mta.ca; Mon, 02 Feb 2009 17:31:37 -0400 Date: Mon, 2 Feb 2009 18:53:01 +1100 (EST) Subject: categories: Re: Question on "On Closed Categories of Functors" From: street@ics.mq.edu.au To: "Tony Meman" , "categories" MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: street@ics.mq.edu.au Message-Id: Status: O X-Status: X-Keywords: X-UID: 6 > Let V be a symmetric monoidal closed category and C a small V-category. > Brian Day constructs a symmetric monoidal closed structure ([C,V],@,E) = on > the V-category of V-functors [C,V] for some cases [3.3, 3.6], e.g. if > (C,*,e) is a symmetric monoidal V-category [4.1]. The underlying > *category* > [C,V] of V-functors admits a closed symmetric monoidal structure from t= he > enriched one by taking the underlying functor of each V-functor, the > underlying natural transformation of each V-natural transformation. > > Because a closed symmetric monoidal category is canonically enriched ov= er > itself, the category [C,V] gets a [C,V] enrichment in this way. > > My question is: What does this [C,V]-enrichment of [C,V] have to do wit= h > the V-enrichment of [C,V]? > Suppose C have a terminal object t. One gets a evaluation functor > Ev_t:[C,V]-CAT-->V-CAT. Is this the connection between the two enrichme= nts? I think what you want here is the following observation. Every closed monoidal V-category E is also an E-category. The unit object j for tensor in E is a monoid and so E(j,-) : E --> V is a monoidal V-functor. Therefore by applying it on hom objects, it induces a 2-functor E-Cat --> V-Cat. In particular, you can apply the 2-functor to E itself to see it as a V-category. Your example is for E =3D [C,V]. Ross PS I have ordinary- (not enriched-) mailed your message to Brian himself. He may want to add something when he gets it. But I hope I have the story you need! From rrosebru@mta.ca Tue Feb 3 10:22:31 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Feb 2009 10:22:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LUM8p-0003RT-Dy for categories-list@mta.ca; Tue, 03 Feb 2009 10:20:43 -0400 Date: Mon, 02 Feb 2009 15:43:16 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: "Kantor dust" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 7 Prof. Peter Johnstone wrote: > A topos with a Cantor set object (i.e. a final coalgebra for FX = X+X) > necessarily has a natural number object. Observe that the Cantor set K > necessarily has a point (since 1 has an F-coalgebra structure), so the > isomorphism K+K \cong K yields a monomorphism K \to K and a point > disjoint from its image. From there on, use Corollary D5.1.3 in the > Elephant. Oh, of course: pick a point out of one half and recurse on the other. Very plausible that that would work in any topos, but it's great to be able to stare at an actual proof. Thank you! How about the converse: does N entail K? In any topos with NNO N the underlying object of the final coalgebra of FX = X+X is presumably 2^N. Does the Elephant prove that 2^N can be made a final coalgebra of X+X? And if so, what other coalgebras are brought into existence by N? For example can N^N be made a doubly inductive (inductive-coinductive) coalgebra encoding the lexicographic order that gives N^N the order type of the nonnegative reals? That would give a pretty direct construction of the usual topology of the real line in any topos with NNO. (This is the one-dimensional conception of the continuum, as opposed to the zero-dimensional conception preferred by descriptive set theorists, who take the continuum to be N^N with the ordinary product topology.) Does \Omega^N as the final coalgebra for FX = \Omega x X ever arise in practical situations where \Omega is more than just a pointed version of 1+1 as in Set, e.g. graph theory? Vaughan Pratt From rrosebru@mta.ca Tue Feb 3 20:12:06 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 03 Feb 2009 20:12:06 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LUVKt-0000tQ-SP for categories-list@mta.ca; Tue, 03 Feb 2009 20:09:47 -0400 Date: Tue, 3 Feb 2009 17:59:58 +0000 (GMT) From: "Prof. Peter Johnstone" To: Vaughan Pratt , categories list Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Prof. Peter Johnstone" Message-Id: Status: RO X-Status: X-Keywords: X-UID: 8 On Mon, 2 Feb 2009, Vaughan Pratt wrote: > How about the converse: does N entail K? In any topos with NNO N the > underlying object of the final coalgebra of FX = X+X is presumably 2^N. > Does the Elephant prove that 2^N can be made a final coalgebra of X+X? > It's not in the Elephant; but it's an easy exercise in primitive recursion, given a coalgebra structure X \to X + X, to define the transpose N x X \to 2 of the unique coalgebra morphism X \to 2^N. > And if so, what other coalgebras are brought into existence by N? For > example can N^N be made a doubly inductive (inductive-coinductive) > coalgebra encoding the lexicographic order that gives N^N the order type > of the nonnegative reals? That would give a pretty direct construction > of the usual topology of the real line in any topos with NNO. (This is > the one-dimensional conception of the continuum, as opposed to the > zero-dimensional conception preferred by descriptive set theorists, who > take the continuum to be N^N with the ordinary product topology.) > How do you (constructively) give N^N the order type of the nonnegative reals? I know how to give it the order type of the irrationals, but that's still zero-dimensional. However, Freyd's presentation of the real unit interval as a final coalgebra is done constructively (for any topos with NNO) in the Elephant, D4.7.17. Peter Johnstone From rrosebru@mta.ca Wed Feb 4 16:06:22 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 04 Feb 2009 16:06:22 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LUnzj-0007Cg-CY for categories-list@mta.ca; Wed, 04 Feb 2009 16:05:11 -0400 From: Gaucher Philippe To: categories@mta.ca Subject: categories: Preprint : Directed algebraic topology and higher dimensional transition system Date: Wed, 4 Feb 2009 10:09:25 +0100 MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Gaucher Philippe Message-Id: Status: O X-Status: X-Keywords: X-UID: 9 Dear all, here is a new preprint. Best regards. pg. Title: Directed algebraic topology and higher dimensional transition system Abstract : Cattani-Sassone's notion of higher dimensional transition system is interpreted as a small-orthogonality class of a locally finitely presentable topological category of weak higher dimensional transition systems. In particular, the higher dimensional transition system associated with the labelled $n$-cube turns out to be the free higher dimensional transition system generated by one $n$-dimensional transition. As a first application of this construction, it is proved that the category of higher dimensional transition systems is equivalent to a full reflective subcategory of the category of labelled symmetric precubical sets. As a second application, it is given a factorization of the mapping taking a CCS process name to a flow through higher dimensional transition systems. The second application of this paper can be easily adapted to other process algebras and to other topological models of concurrency than the one of flows. URL: http://www.pps.jussieu.fr/~gaucher/HDAparadigm.pdf From rrosebru@mta.ca Wed Feb 4 16:06:22 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 04 Feb 2009 16:06:22 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LUnz7-00077n-2b for categories-list@mta.ca; Wed, 04 Feb 2009 16:04:33 -0400 Content-class: urn:content-classes:message MIME-Version: 1.0 Subject: categories: Fields Workshop on Smooth Structures in Logic, Category Theory and Physics Date: Tue, 3 Feb 2009 20:55:48 -0500 From: "Pieter Hofstra" To: Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: "Pieter Hofstra" Message-Id: Status: O X-Status: X-Keywords: X-UID: 10 Fields Institute Workshop, Second Announcement: Smooth Structures in Logic, Category Theory and Physics University of Ottawa May 1-3, 2009 Registration is now open: people can register online at http://www.fields.utoronto.ca/programs/scientific/08-09/smoothstructures/= Students who wish to apply for financial support can do so through this = website. Since we have a limited budget for student support it is = recommended to apply for this as soon as possible. Anyone who wishes to contribute a talk is requested to contact one of = the organizers. In case there are more talks than available time slots = the organizers will make a selection. The local website has information on hotels and B&B's near campus: http://aix1.uottawa.ca/~scpsg/Fields09/Fields09.smoothworkshop.html With best regards, Richard Blute (rblute@uottawa.ca) Pieter Hofstra (phofstra@uottawa.ca) Philip Scott (phil@site.uottawa.ca) Michael Warren (mwarren@uottawa.ca) From rrosebru@mta.ca Thu Feb 5 09:17:57 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Feb 2009 09:17:57 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LV45d-0006Rf-EY for categories-list@mta.ca; Thu, 05 Feb 2009 09:16:21 -0400 Date: Wed, 4 Feb 2009 23:14:00 -0800 (PST) From: John Edward Subject: categories: Draft paper submission deadline extended: Category Theory To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: John Edward Message-Id: Status: RO X-Status: X-Keywords: X-UID: 11 Draft paper submission deadline extended: Category Theory =A0=20 The deadline for draft paper submission at the 2009 International Conferenc= e on Theoretical and Mathematical Foundations of Computer Science (TMFCS-09= ) (website: http://www.PromoteResearch.org ) is extended due to numerous re= quests from the authors. As a result, the deadline for paper submission for= the special session on Category Theory is also extended accordingly. The c= onference and the session will be held during July 13-16 2009 in Orlando, F= L, USA. The conference will take place at the same time and venue where sev= eral other international conferences are taking place. The other conference= s include:=20 =B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Artificial Intellig= ence and Pattern Recognition (AIPR-09)=20 =B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Automation, Robotic= s and Control Systems (ARCS-09)=20 =B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Bioinformatics, Com= putational Biology, Genomics and Chemoinformatics (BCBGC-09)=20 =B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Enterprise Informat= ion Systems and Web Technologies (EISWT-09)=20 =B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on High Performance Co= mputing, Networking and Communication Systems (HPCNCS-09)=20 =B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Information Securit= y and Privacy (ISP-09)=20 =B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Recent Advances in = Information Technology and Applications (RAITA-09)=20 =B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Software Engineerin= g Theory and Practice (SETP-09)=20 =B7=A0=A0=A0=A0=A0=A0=A0=A0 International Conference on Theory and Applicat= ions of Computational Science (TACS-09)=20 =A0=20 The website http://www.PromoteResearch.org contains more details.=20 =A0=20 Sincerely=20 John Edward=20 Publicity committee=20 =A0 =0A=0A=0A From rrosebru@mta.ca Thu Feb 5 09:17:57 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Feb 2009 09:17:57 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LV44l-0006Jv-C9 for categories-list@mta.ca; Thu, 05 Feb 2009 09:15:27 -0400 Date: Wed, 04 Feb 2009 12:24:41 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: "Kantor dust" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: RO X-Status: X-Keywords: X-UID: 12 Prof. Peter Johnstone wrote: > On Mon, 2 Feb 2009, Vaughan Pratt wrote: > >> How about the converse: does N entail K? In any topos with NNO N the >> underlying object of the final coalgebra of FX = X+X is presumably 2^N. >> Does the Elephant prove that 2^N can be made a final coalgebra of X+X? >> > It's not in the Elephant; but it's an easy exercise in primitive > recursion, given a coalgebra structure X \to X + X, to define the > transpose N x X \to 2 of the unique coalgebra morphism X \to 2^N. Ah, good, thanks. In that case it should be almost as easy, given a suitably "easy" coalgebra structure X --> N x X, to define the transpose N x X --> N of the unique coalgebra morphism X --> N^N. > How do you (constructively) give N^N the order type of the nonnegative > reals? The easiest one is forward lexicographic order (s < t when s(i) < t(i) at the least i where distinct sequences s and t differ), which has the order type of [0,oo), equivalently [0,1). One way to see this is to replace the 0's in the usual binary expansion of x \in [0,1) by commas and read the resulting comma-separated blocks of 1's as tally notation. Alternatively, any monotone bijection f: [0,oo) --> [0,1), such as x/(x+1) giving one kind of continued fraction, or 2*atan(x)/pi for "circular continued fractions", induces the monotone bijection R: N^N --> [0,oo) defined coinductively as R(s) = s(0) + f(R(s o succ)). These are among the coalgebraic presentations of the reals Dusko Pavlovic and I spoke about in Amsterdam on 3/20/99 at CMCS, see ENTCS 19, 133-147 (1999), journal version TCS 280(1-2):105-122 (2002). > I know how to give it the order type of the irrationals, but > that's still zero-dimensional. Reverse lexicographic order gives the irrationals, and is the one usually encountered with the continued fractions used by "spigot algorithm" programmers such as Bill Gosper, who don't seem to mind that the space they're working in is totally disconnected. This results from not bothering to correct for the antimonotonicity of 1/(x+1). Pedantic spigot programmers who prefer working in a connected space can easily substitute its monotonic complement, 1-1/(x+1) = x/(x+1), but (digressing from mathematical reality for a moment) to what practical advantage? Presumably Brouwer would take Gosper's side here, it's not as if the real line is going to crumble into dust when it becomes totally disconnected by omitting a countable subset, it's still held together by its metric. Nature abhors topology. A demonstrably nondiscrete Hausdorff space in either nature or computer engineering would be a great discovery worthy of the Nobel prize in physics or the Turing award respectively. Back to mathematical reality. > However, Freyd's presentation of the > real unit interval as a final coalgebra is done constructively (for any > topos with NNO) in the Elephant, D4.7.17. Freyd's post of 12/22/99 to this list introducing his presentation, http://north.ecc.edu/alsani/ct99-00(8-12)/msg00039.html gives the general provenance for the coalgebraic approach to the reals as our CMCS paper. Our respective approaches to connecting up the bits of our coalgebras to form a continuum differ mainly in that Peter explicitly glues the abutting ends of 2xX ~ X+X together while we exploit the open-ended nature of N (least but no greatest element, as the discretization of a half-open interval) for a glue-less connection at the expense of the additional induction needed when replacing 2 by N. The choice of poisons is therefore manual glue vs. double induction. In light of your remark at the start of D4.7 that "there are different constructions of the reals which are classically equivalent but may yield different results in a non-Boolean topos," is there a topos in which the order type of the Freyd coalgebra is not that of the (forward) lexicographic ordering of N^N (modulo endpoints)? Are they the same in Grph, for example? Vaughan Pratt From rrosebru@mta.ca Thu Feb 5 23:53:35 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 05 Feb 2009 23:53:35 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LVHkW-0001aP-U2 for categories-list@mta.ca; Thu, 05 Feb 2009 23:51:28 -0400 Date: Thu, 5 Feb 2009 13:44:02 -0800 From: Toby Bartels To: categories list Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 13 Vaughan Pratt wrote in part: >Prof. Peter Johnstone wrote: >>How do you (constructively) give N^N the order type of the nonnegative >>reals? >One way to see this is to replace the 0's in the usual binary expansion >of x \in [0,1) by commas and read the resulting comma-separated blocks >of 1's as tally notation. 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. >is there a topos in >which the order type of the Freyd coalgebra is not that of the (forward) >lexicographic ordering of N^N (modulo endpoints)? 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. --Toby From rrosebru@mta.ca Sat Feb 7 08:52:31 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Feb 2009 08:52:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LVmdG-0006rr-Iz for categories-list@mta.ca; Sat, 07 Feb 2009 08:50:02 -0400 Date: Fri, 06 Feb 2009 16:37:11 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: "Kantor dust" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 14 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? 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. Are these constructively different from the binary reals? And if so, is there any intuition underlying that difference that is as clear-cut as the difference between either and the Dedekind reals? > >> is there a topos in >> which the order type of the Freyd coalgebra is not that of the (forward) >> lexicographic ordering of N^N (modulo endpoints)? > > 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. But neither will the nonconstant functions from N^N to N be continuous with respect to the order interval topology on N^N lexicographically ordered. So I don't see any progress here towards distinguishing the order type of the Freyd coalgebra from the lexicographic order on N^N, in this topos or any other. Vaughan Pratt From rrosebru@mta.ca Sat Feb 7 16:06:00 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 07 Feb 2009 16:06:00 -0400 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 Date: Sat, 7 Feb 2009 17:18:29 +0000 (GMT) From: "Prof. Peter Johnstone" To: Vaughan Pratt , categories list Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Prof. Peter Johnstone" Message-Id: Status: O X-Status: X-Keywords: X-UID: 15 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 From rrosebru@mta.ca Sun Feb 8 09:52:32 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 08 Feb 2009 09:52:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWA3I-0001os-Pn for categories-list@mta.ca; Sun, 08 Feb 2009 09:50:28 -0400 Date: Sun, 8 Feb 2009 12:56:53 +0100 From: gcuri@math.unipd.it To: categories@mta.ca Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: gcuri@math.unipd.it Message-Id: Status: O X-Status: X-Keywords: X-UID: 16 Quoting "Prof. Peter Johnstone" : > > 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 poin= t > > that whereas Cauchy reals can be understood constructively as a set, = any > > attempt to make Dedekind's reals constructive turns them into a prope= r > > class. > > > > Between Dedekind cuts and Cauchy sequences, the more appropriate noti= on > > 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. Even if one insists that constructive entails predicative the appropriate= ness of Cauchy reals is questionable: Lubarsky and Rathjen prove in fact that in = a=20 subsystem of CZF (Aczel' constructive set theory), i.e., in CZF with Subset Collection replaced by exponentiation, the Dedekind reals form a = proper class. In ordinary CZF (that has no choice principle and no powersets), the Dedekind reals *do* form a set (Aczel & Rathjen), as do more generall= y the points of any weakly set-presented T^*_1 locale (Aczel & Curi), in particular of any locally compact regular one. It is also useful to recall that (in "On the Cauchy Completeness of the Constructive Cauchy Reals", MLQ, 53, No. 4-5 (2007), pp. 396-414) Lubarsky has proved that the Cauchy Reals are not complete in intuitioni= stic set theory without choice. There's then the point of view that, constructively, the reals should be considered as a `space', rather than a set, and that in this perspective = they are more properly regarded e.g. as a locale/formal space (rather than as = a set/class of points with a topology)... Regards, Giovanni Curi ----------------------------------------------------------------- This message was sent using IMP, the Internet Messaging Program. Dipartimento di Matematica Pura ed Applicata Universita' degli Studi di Padova www.math.unipd.it From rrosebru@mta.ca Sun Feb 8 09:52:32 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 08 Feb 2009 09:52:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWA2p-0001nu-3U for categories-list@mta.ca; Sun, 08 Feb 2009 09:49:59 -0400 Date: Sat, 7 Feb 2009 14:58:19 -0800 From: Toby Bartels To: categories list Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 17 Prof. Peter Johnstone wrote in part: >Vaughan Pratt wrote: >>Whose reals, Cauchy's or Dedekind's? >Toby was of course referring to the Dedekind reals Actually, I was trying to keep it open, since different schools of constructivism have different opinions about which are the correct reals (as well as which are equivalent). But nobody uses the binary reals, since they can't subtract them. (To get the first digit of 0.1000000000... - 0.01000000000..., you need to know which sequence, if either, stops repeating first.) I agree that one would default to Dedekind reals (or something equivalent), since that seems to be agreed on by the "practising" schools (that is, those constructivists trying to do ordinary mathematics, albeit constructively, rather than doing metamathematics). >>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. I'll have to read what they mean, but to say ~any~ attempt seems too strong. Even in a predicative theory, countable choice implies their equivalence, so are they claiming that countable choice is not constructive? (In my experience, Fred Richman is the only practising non-finitist analyst who doubts both excluded middle and countable choice.) The Dedekind reals can also be constructed in CZF (Peter Aczel's predicative constructive set theory) even if you remove countable choice, using subset collection aka fullness. Similarly, if you remove identity types from intensional type theory (so breaking the justification of countable choice), you can still justify the fullness axiom and so construct the Dedekind reals (albeit not literally as sets of rational numbers). >>Between Dedekind cuts and Cauchy sequences, the more appropriate notion >>of reals for constructive analysis would surely be the Cauchy reals. The experience in measure theory and Banach space theory since the 1980s suggests that a Dedekind-complete ordered field is needed. The only question is whether such a thing exists; most believe it does. (If countable choice or excluded middle holds, the Cauchy reals work, which takes care of nearly every practising analyst, constructive or not. Fred Richman, the only exception I know, still uses the Dedekind reals, although that's easy for him since he is not predicativist.) Note: everything above is about the ~located~ Dedekind reals; a located Dedekind cut is a pair (L,U) of order-open inhabited sets such that r in L and s in U => r < s => r in L or s in U. This is what Freyd's coalgebra construction produces, and it's what practising analysts want to use. --Toby From rrosebru@mta.ca Sun Feb 8 16:39:57 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 08 Feb 2009 16:39:57 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWGQu-0002qe-G5 for categories-list@mta.ca; Sun, 08 Feb 2009 16:39:16 -0400 Mime-Version: 1.0 (Apple Message framework v624) Content-Transfer-Encoding: 7bit From: Paul Taylor Subject: categories: Re: "Kantor dust" Date: Sun, 8 Feb 2009 15:03:04 +0000 To: Categories list Sender: categories@mta.ca Precedence: bulk Reply-To: Paul Taylor Message-Id: Status: O X-Status: X-Keywords: X-UID: 18 There have been several very interesting comments on this thread, but I would like to repeat my request that people should be clear about WHICH OF MANY "CONSTRUCTIVE" THEORIES OF MATHEMATICS they mean as the context of their comments. There are, as I said, interesting mathematical points to be made, both within each of these theories, and by comparing them. However, without a clear statement of the foundational context, the discussion degenerates. The original question was about Cantor space, rather than either the Cauchy or Dedekind reals. If you want to construct Cantor space from the reals by the "missing third" construction, I would think that it makes little difference whether you start from Cauchy or Dedekind. Or, indeed, from binary sequences, which of course form a Cantor space in the first place, so that is really a question of how to construct the reals from Cantor space rather than vice versa. Vaughan Pratt said > between Dedekind cuts and Cauchy sequences, the more appropriate notion > of reals for constructive analysis would surely be the Cauchy reals and I am certainly aware that, as a sociological fact, many type theorists and exact real arithmetic programmers believe this. Can anybody point me to a reasoned critique, or justification of the view that Cauchy sequences are "more appropriate" for purposes such as these? All that I have ever heard is essentially a condemnation of Dedekind for the "heresy" of impredicativity, uncountability, non-computability, being a proper class, etc. I gave a lecture (see PaulTaylor.EU/slides) entitled "In defence of Dedekind and Heine--Borel", which I presented as if I were an advocate in a court of law. Several type theorists and constructive analysts were present. Beforehand, I had asked around for a statement of "the case against Dedekind", but nobody seemed to be able to state it for me. Five years ago I had no opinion whatever on these matters, but, as you gather, I now consider that both Dedekind completeness and the Heine-- Borel theorem are essential parts of "constructive" analysis. Of course, I think that because the reals in Abstract Stone Duality satisfy them (and because it puts me in agreement with mainstream analysts). However, ASD is a recursively axiomatised and enumerable theory. I don't like the notions of (un)countability or (im)predicativity, but, if you must apply them, ASD is countable and predicative. Regarding computation, last year Andrej Bauer gave a "proof of concept" demonstration that one can compute efficiently with Dedekind reals in the ASD language for R. This of course uses interval arithmetic, but in fact it also makes extremely novel use of back-to-front ("Kaucher") intervals, which appear but are very badly presented in the interval analysis literature. I have been trying to persuade him to make this work publicly available. Since I'm talking about the reals in ASD, I should say what the difference is between the Cauchy and Dedekind reals is there. I haven't actually written out a construction of the Cauchy reals, but the evidence that I do have is that THEY ARE THE SAME. More precisely, Dedekind completeness is inter-derivable with sobriety for R, just as definition by description is equivalent to sobriety of N. This means that if you construct the "Cauchy reals" as a quotient of Cantor space by an equivalence relation (this is known as the "signed binary" representation of reals) within ASD then the result will be Dedekind complete. The details of this are set out in Section 14 of "The Dedekind reals in ASD" by Andrej and me, www.PaulTaylor.EU/ASD/dedras I think it is worth making a note of Vaughan's earlier comment that > In concrete Stone duality, increasing structure on one side is offset > by > decreasing structure on the other. One would hope for a similar > phenomenon in abstract Stone duality. > > If we can consider constructivity as part of the structure of an > object, > then we should expect that the more constructive some type of object, > the less constructive the "object of all objects of that type." So > for > example if (total) recursive functions are demonstrably more > constructive than partial recursive functions by some criterion, we > should expect the set of all recursive functions to be *less* > constructive than that of partial recursive functions by the same > criterion, rather than more. > > The phenomena you're observing here seem entirely consistent with this > principle, and point up the need to be clear, when judging > constructivity in some context, whether it is the collection or the > individuals therein being so judged, with the added complication that > Stone duality makes the roles of collection and individual therein > interchangeable, such as when elements of sets are understood as > ultrafilters of Boolean algebras. However, I think that the Galois--Stone contravariance applies WITHIN a particular foundational system, and not to VARIATIONS of the degree of constructivity. Indeed, the usual experience in setting up a Galois connection or Stone adjunction is that, in order to make the comparison work at all, you need to make additional assumptions. Paul Taylor From rrosebru@mta.ca Sun Feb 8 16:39:57 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 08 Feb 2009 16:39:57 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWGQH-0002oB-Qf for categories-list@mta.ca; Sun, 08 Feb 2009 16:38:37 -0400 Date: Sun, 8 Feb 2009 14:51:19 +0000 (GMT) From: "Prof. Peter Johnstone" To: Toby Bartels , Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Prof. Peter Johnstone" Message-Id: Status: O X-Status: X-Keywords: X-UID: 19 On Sat, 7 Feb 2009, Toby Bartels wrote: >> Toby was of course referring to the Dedekind reals > > Actually, I was trying to keep it open, > since different schools of constructivism have different opinions > about which are the correct reals (as well as which are equivalent). > But nobody uses the binary reals, since they can't subtract them. Never mind subtraction -- you can't even add them. As I mentioned in my last posting, the question "Is x < 1/2?" is decidable for Vaughan's binary reals, but "Is x < 1/3?" is not (constructively), so the operation of adding 1/6 can't be defined. Peter Johnstone From rrosebru@mta.ca Mon Feb 9 13:04:35 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Feb 2009 13:04:35 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWZVh-0000T8-C1 for categories-list@mta.ca; Mon, 09 Feb 2009 13:01:29 -0400 MIME-version: 1.0 Message-id: <8C91305E-226A-4D07-9604-9BA021A27B4F@me.com> From: Steve Stevenson To: Toby Bartels , Subject: categories: Re: "Kantor dust" Date: Sun, 08 Feb 2009 15:36:37 -0500 Content-type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-transfer-encoding: 7BIT Sender: categories@mta.ca Precedence: bulk Reply-To: Steve Stevenson Status: O X-Status: X-Keywords: X-UID: 20 On Feb 7, 2009, at 5:58 PM, Toby Bartels wrote: > Prof. Peter Johnstone wrote in part: > >> Vaughan Pratt wrote: > >>> Whose reals, Cauchy's or Dedekind's? > >> Toby was of course referring to the Dedekind reals How about IEEE 754 reals? They're really "scientific notation". There has been a tremendous amount of work on them by William Kahan and others and now are the standard for the numerical analysis world and computers. Since this is the basics for computation, I'd propose that they can be tightened up even more to suit constructivist purposes. Steve -------- D. E. Stevenson, Department of Computer Science Director, Institute for Modeling and Simulation Applications Clemson University, Clemson, SC 29634-0974 From rrosebru@mta.ca Mon Feb 9 13:04:36 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Feb 2009 13:04:36 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWZYd-0000nY-TQ for categories-list@mta.ca; Mon, 09 Feb 2009 13:04:31 -0400 Date: Sun, 8 Feb 2009 16:31:34 -0800 From: Toby Bartels To: categories list Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 21 Steve Stevenson wrote in part: >How about IEEE 754 reals? They're really "scientific notation". There >has been a tremendous amount of work on them by William Kahan and others >and now are the standard for the numerical analysis world and computers. >Since this is the basics for computation, I'd propose that they can be >tightened up even more to suit constructivist purposes. Floating-point reals have terrible theoretical properties; they're not even a ring (not even classically). This is why even after all of Kahan's good work on algorithms, rounding errors are unavoidable (the "Table-Maker's Dilemma"). A floating-point real basically consists of a rational number x together with a rational maximum error e, subject to the condition that, for some integer n, 10^n x is an integer and e = 10^{-n}/2. (There is some redundancy in this simplified description.) This is not acceptable constructively, since one cannot prove (even with countable choice, impredicative power sets, etc) that every real number has such a floating-point representation. At the very least, one must add some epsilon to the maximum e; to keep it simple, I would set e to 10^{-n} (so that 1.6 is acceptable as the result of 5/3, although good algorithms would probably give 1.7). This would remove rounding errors from the Table-Maker's Dilemma. I believe (but I may be wrong through unfamiliarity with the literature) that most researchers prefer instead to allow arbitrarily large e, thus using interval arithmetic, even though this is more complicated. (Actual implementations of floating-point arithmetic usually also have maximum allowed values of both n and 10^n x, leading to rounding errors from underflow and overflow. However, overflow errors already arise in natural-number arithmetic, so this is not really the fault of the floating-point idea. One can delay all such errors until run-time memory limits.) --Toby From rrosebru@mta.ca Mon Feb 9 13:08:04 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Feb 2009 13:08:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWZbu-0001Bx-OX for categories-list@mta.ca; Mon, 09 Feb 2009 13:07:54 -0400 Date: Sun, 8 Feb 2009 17:30:31 -0800 From: Toby Bartels To: Categories list Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 22 Paul Taylor wrote in part: >Can anybody point me to a reasoned critique, or justification of the >view that Cauchy sequences are "more appropriate" for purposes such >as these? All that I have ever heard is essentially a condemnation >of Dedekind for the "heresy" of impredicativity, uncountability, >non-computability, being a proper class, etc. >I gave a lecture (see PaulTaylor.EU/slides) entitled "In defence of >Dedekind and Heine--Borel", which I presented as if I were an >advocate in a court of law. Several type theorists and constructive >analysts were present. Beforehand, I had asked around for a statement >of "the case against Dedekind", but nobody seemed to be able to state >it for me. Besides the case that you present briefly in your slides, there is this: The Cauchy reals exist an a Pi-W-pretopos (equivalently, in a constructive set or type theory with exponentiation but no power sets or even fullness and with infinity but no countable choice). But the Dedekind reals, as far as I can tell, do not; excluded middle, power sets, fullness, or countable choice would each do the job, but you need ~something~. (ASD takes another approach, of course.) And while I don't know any non-finitist practising constructivists that doubt all of these, I do know at least one that doubts each. Thus practising constructivists may happily use the Dedekind reals, while formalists that want to cover all practising schools find that they are not quite available in the obvious common denominator. (Actually, Brouwer intuitionists don't really even accept exponenenation, although they do accept N^N and AC_00 so do have Cauchy = Dedekind reals.) I don't find this argument conclusive; the proper course is either to accept the existence of the Dedekind reals as an axiom (since everybody believes it, even if for different reasons) or just to give up on point-set topology and use locales (although these require subtlety to use predicatively). But it's there, and it probably explains some logicians' positions. >However, ASD is a recursively axiomatised and enumerable >theory. I don't like the notions of (un)countability or >(im)predicativity, but, if you must apply them, ASD is countable >and predicative. But ASD with the underlying-set axiom is impredicative, yes? I really like ASD, so don't interpet my post as opposition to your position, but rather an attempt to clarify what the opposition may be thinking. --Toby From rrosebru@mta.ca Mon Feb 9 13:12:35 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Feb 2009 13:12:35 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWZgH-0001f3-1n for categories-list@mta.ca; Mon, 09 Feb 2009 13:12:25 -0400 From: Thomas Streicher Date: Mon, 9 Feb 2009 12:49:38 +0100 To: categories@mta.ca Subject: categories: Dedekind versus Cauchy reals MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Thomas Streicher Message-Id: Status: O X-Status: X-Keywords: X-UID: 23 Paul has asked why most constructivists have a preference for Cauchy numerals. Well, most constructivists haven't since under the widely accepted AC_N they coincide. This, of course, doesn't deny the fact that in many sheaf toposes AC_n fails. But from point of view of the BHK interpretation AC_N is most natural. But I think the reason for prefering Cauchy over Dedekind has a quite pragmatic reason. What you are interested in is a Cauchy sequence of reals with a fixed rate of convergence (ensuring e.g. that the n-th item has distance < 2^{-n} to the limit). AC_N of course allows you to magically find a modulus of convergence for every Cauchy sequence. But like Church's Thesis or Brouwer's Theorem this is sort of a Deus ex machina (actually those are 2 contradictory dei ex machina!) and thus of moderate help for exact computation on the reals. If you base your reals on Dedekind's idea you may certainly compute with them but the result isn't very telling because a computable Dedkind real is a semidecision procedure telling you whether a given rational interval contains the (ideal) real under consideration. This doesn't help you at all to compute the real up to a given precision because you have to first guess the right interval. Of course, you may consider a partition of some area of guesses and apply the semidecision procedure to all those intervals in parallel. But that's very inefficient and can't be implemented within usual sequential programming languages. Thomas From rrosebru@mta.ca Mon Feb 9 14:51:50 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 09 Feb 2009 14:51:50 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWbDR-0004d2-5V for categories-list@mta.ca; Mon, 09 Feb 2009 14:50:45 -0400 MIME-Version: 1.0 Date: Mon, 9 Feb 2009 12:26:32 +0100 Subject: categories: symmetric monoidal adjunctions From: Tony Meman To: categories Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Tony Meman Message-Id: Status: O X-Status: X-Keywords: X-UID: 24 Dear category theorists, I have a question concerning symmetric monoidal adjunctions (of symmetric monoidal functors). Let V and W be symmetric monoidal categories, C a small category, F, G symmetric monoidal functors and F:V<-->W:G a symmetric monoidal adjunction. Is f:Fun(C,V)<-->Fun(C,W):g a symmetric monoidal adjunction? The functor categories Fun(C,V) and Fun(C,W) are endowed with the pointwise symmetric monoidal structure and the functors f and g are defined pointwise, too. I am sorry that I have to ask you all this things about monoidal categories and enriched categories but I can't find a book on that. I would be very pleased if anybody can suggest me something to read. Thank you in advance for any help. Tony From rrosebru@mta.ca Tue Feb 10 08:29:39 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 10 Feb 2009 08:29:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWrjN-0000Be-87 for categories-list@mta.ca; Tue, 10 Feb 2009 08:28:49 -0400 Date: Mon, 9 Feb 2009 22:47:56 +0000 (GMT) From: "Prof. Peter Johnstone" To: Dusko Pavlovic , Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Prof. Peter Johnstone" Message-Id: Status: O X-Status: X-Keywords: X-UID: 25 On Mon, 9 Feb 2009, Dusko Pavlovic wrote: > QUESTION 1: re peter johnstone's > >> > > 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. > > are you claiming that this statement is true with respect to every base topos > and every real line in it? (the discussion seems to have touched upon the > various constructions of the various real lines. it would be nice to know > where is the one, over which you build the topos, is coming from.) > That's actually a quote from Toby Bartels, not from me. It's a statement about a topos built over the classical topos of sets; the argument is a rather ad hoc one, and I'm not sure to what extent it's possible to make it constructive. However, as I said elsewhere, I prefer to work with the gros topos of spaces (i.e. sheaves on a suitable full subcategory of spaces for the coverage consisting of jointly- surjective families of open inclusions) and there it's quite clear what you need: namely, Heine--Borel (equivalently, exponentiability of R in your category of spaces). That's not true in all toposes; you could try to get round it by basing your gros topos on locales rather than spaces (the locale of formal reals being constructively locally compact), but it's not clear (to me, at least) what the result would actually mean if you based yourself on a topos where the formal reals aren't spatial. > QUESTION 2: is there a branch of constructivism that would reject as > non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as the > coefficients of continued fractions? > I don't think there is any doubt that the map exists. The problem is that, for most if not all schools of constructivism, it's wildly non-surjective. Peter Johnstone From rrosebru@mta.ca Tue Feb 10 08:29:39 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 10 Feb 2009 08:29:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWriU-000088-W1 for categories-list@mta.ca; Tue, 10 Feb 2009 08:27:55 -0400 Date: Mon, 9 Feb 2009 22:18:44 +0000 (GMT) From: Dusko Pavlovic To: "Prof. Peter Johnstone" , Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Dusko Pavlovic Message-Id: Status: O X-Status: X-Keywords: X-UID: 26 hi. i missed most of this thread, but even this one message that i did catch raises several questions that i would like to share. QUESTION 1: re peter johnstone's >>> 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. are you claiming that this statement is true with respect to every base topos and every real line in it? (the discussion seems to have touched upon the various constructions of the various real lines. it would be nice to know where is the one, over which you build the topos, is coming from.) QUESTION 2: is there a branch of constructivism that would reject as non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as the coefficients of continued fractions? COMMENT: IF the answer to either of the above questions is NO, then maybe the tacit SLOGAN that "constructively valid" = "true in every topos" needs to be taken *very carefully*. when we build toposes over classical universes, then we may be able to force away more than any constructivist would ever reject. the strict constructivist logics have already been marginalized as too restrictive; lets not completely bury them just for the joy of constructing counterexamples. moreover, EVEN IF the answer to both of the above questions is YES, the above SLOGAN still does not tell the whole story, IMHO. the constructivists wanted to make our computations effective. that goal led to some great philosophical debates in the first half of XX century. later people built computers and paid lots of programmers to make computations effective. besides brouwer, and heyting and kolmogorov, maybe we should admit that people like gosper, and knuth, and dijkstra, and our own vaughan pratt, also have an idea about what is effectively computable. peter johnstone points out that the comparison test for the binary reals (i presume the reals in base 2; there are many other representations, of course) is undecidable. this actually applies to every base, and even to the continued fraction representation (because it is irredundant). but in the practice of effective computations, this is no showstopper. there are many things that need to be computed with the reals, and no one representation fits for all purposes. so the statement > nobody uses the binary reals probably has more counterexamples than, say, the statement "nobody uses toposes". even if "the" binary reals were completely wrong. the study of the various effective algebraic operations on the reals, always reduced to one binary form or another, goes back at least to gosper and schroepel, the original "hackers" from the 70s. they were, of course, aware that the comparison test was undecidable. buyt people prefer to run a program that may not terminate, or will terminate fast, over a program guaranteed to terminate between tomorrow and 2 years from now. gosper's continued fraction representation was improved by jean vuillemin, who proposed in 1990s a redundant representation, where the comparison test is decidable. this is what at least some people have really been using in their real projects, sensitive enough to bring the chaotic effects of the floating point arithmetic to the surface. it would be interesting to understand whether the notion of computability as embodied in toposes is related in some rational way with the notion of computability as embodied in computers. -- dusko From rrosebru@mta.ca Wed Feb 11 09:39:42 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 09:39:42 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFJI-0002uv-BD for categories-list@mta.ca; Wed, 11 Feb 2009 09:39:28 -0400 MIME-version: 1.0 Content-transfer-encoding: 7BIT Content-type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Message-id: From: Steve Stevenson To: Toby Bartels , Subject: categories: Re: "Kantor dust" Date: Tue, 10 Feb 2009 14:04:11 -0500 Sender: categories@mta.ca Precedence: bulk Reply-To: Steve Stevenson Status: O X-Status: X-Keywords: X-UID: 27 On Feb 8, 2009, at 7:31 PM, Toby Bartels wrote: > Steve Stevenson wrote in part: > >> How about IEEE 754 reals? They're really "scientific notation". >> > > Floating-point reals have terrible theoretical properties; > they're not even a ring (not even classically). > This is why even after all of Kahan's good work on algorithms, > rounding errors are unavoidable (the "Table-Maker's Dilemma"). Being left-handed and old, I'll propose in my dotage that we may be asking the wrong question. In a rewording, what constructive real numbers are there for the purpose of 1. Being a model of an axiomatic characterization of the reals. 2 Being usable in supercomputing to compute values needed for modeling and simulation. Number 1 requires that we have nice theoretical properties. Number 2 requires something that is bounded only the dollars and life span. Those interested in either purpose have (presumedly) a solution for themselves. The first fix for number 2 might be to go to interval arithmetic --- now what do I need to guarantee that the "real number (in 1)" is trapped between two #2 numbers? Given the bandwidth and memory capacity, we should be able to do those things worth doing: H5N1 infection prediction, climate modeling, malaria control, food production ... I'm willing to live with a demonstrably correct approximation given that we are in an uncertain world. I'll never get the exact answer, I'll only get an approximation. Interval guarantees seems interesting to me. --- Steve Stevenson It's not that people don't know, it's so much of what they know ain't so - Josh Billings. From rrosebru@mta.ca Wed Feb 11 09:39:42 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 09:39:42 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFIA-0002oj-3h for categories-list@mta.ca; Wed, 11 Feb 2009 09:38:18 -0400 Date: Tue, 10 Feb 2009 19:03:56 +0100 From: "I. Moerdijk" MIME-Version: 1.0 To: categories@mta.ca Subject: categories: postdoc position in Utrecht Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: "I. Moerdijk" Message-Id: Status: O X-Status: X-Keywords: X-UID: 28 There is a vacancy for a postdoc position in topology at our department in Utrecht. The position is for two or three years, and is funded by the Dutch science organisation NWO. It is part of a specific research project, which in practice means that we are looking for candidates working in the convex hull of stable homotopy theory -- topological field theory -- operads -- higher categories. The starting time is flexible, although we aim to fill the position between 1 August 2009 and 1 January 2010. If you're interested, please send me an email and append your CV. Ieke Moerdijk From rrosebru@mta.ca Wed Feb 11 09:39:43 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 09:39:43 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFH4-0002jJ-B3 for categories-list@mta.ca; Wed, 11 Feb 2009 09:37:10 -0400 Date: Tue, 10 Feb 2009 01:54:06 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: "Kantor dust" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 29 Prof. Peter Johnstone wrote: > On Mon, 9 Feb 2009, Dusko Pavlovic wrote: >> QUESTION 2: is there a branch of constructivism that would reject as >> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N >> as the coefficients of continued fractions? >> > I don't think there is any doubt that the map exists. The problem is that, > for most if not all schools of constructivism, it's wildly non-surjective. There is more than one notion of continued fraction. I suspect you're thinking of one of the more commonly used ones, but in the light of Dusko and my CMCS'99 paper, which talks about a number of notions of continued fraction, I imagine Dusko had one in mind for which the map is classically a bijection, and surely should continue to be so for at least some schools of constructivism. Let me give a (hopefully) careful proof of this here. As I observed in a previous post, the pathological definitions of "continued fraction" giving the behaviour you may be thinking of are those whose coinductive step is antimonotone, e.g. via a function from [0,oo) to (0,1] such as 1/(1+x). These appear in the literature not from any desire to be pathological but merely because they tend to be the first ones that come to mind, and their non-surjectivity is simply not noticed by the naive programmer. In contrast, monotone functions from [0,oo) to [0,1) such as x/(1+x) or 2*atan(x)/pi, with respective inverses x/(1-x) and tan(pi*x/2), do not create this pathology in the continued fractions based on them, and give rise to maps from N^N to [0,1) and [0,oo) that are not only surjective but bijective, as well as monotone increasing with respect to the lexicographic order on N^N. Let R: N^N --> [0,oo) be the strictly monotone increasing function (with respect to the lexicographic order on N^N) defined coinductively as R(s) = s(0) + f(R(s o succ)) where s: N --> N is a sequence in N^N (a function on N), f: [0,oo) --> [0,1) is a strictly monotone increasing function, for example f(x) = x/(1+x), and succ: N --> N is the successor operation of the NNO N. As a (surely constructive!) witness to the surjectivity, indeed bijectivity, of R, define the inverse S: [0,oo) --> N^N of R as follows. (R converts sequences to Reals, which S turns back into Sequences.) S(x)(0) = floor(x) S(x)(n+1) = S(g(x mod 1))(n) where x mod 1 = x - floor(x) and g(x) = x/(1-x) : [0,1) --> [0,oo) is the inverse of f(x) = x/(1+x) : [0,oo) --> [0,1) used in the definition of R. As an aside for any visual thinkers reading this, the picture [0,oo) ~ [0,1)[1,2)[2,3)... may help. This splits [0,oo) into N unit intervals each identifiable with [0,1), each of which is blown back up to [0,oo) (under this identification) by g(x) = x/(1-x). The function S: [0,oo) --> N^N converts nonnegative reals x to sequences of natural numbers by taking the first element of the sequence to be floor(x), thereby selecting one of the unit intervals, leaving x mod 1 to be accounted for within that interval, of type [0,1), which is blown back up to type [0,oo) using g and then inductively converted to the rest of the sequence by S. In this way we drill down into [0,oo) cranking out natural numbers as we drill progressively deeper. For the typing N^N --> [0,1) that Dusko asked about, the codomain of R is easily converted from [0,oo) to [0,1) by composing the monotone bijection f : [0,oo) --> [0,1) with the monotone bijection R : N^N --> [0,oo) to give a monotone bijection from N^N to [0,1). In the topos of sheaves on either R itself or the subcategory of Top you prefer, I am not a topos hacker and have no idea whether there are more than two functions from N^N to 2 = 1+1 when N^N is defined coinductively as a final coalgebra (as distinct from being defined simply by exponentiation, where surely there are more than two such functions). Toby Bartels claims it's obvious, in which case there should be a short construction of a nonconstant function from N^N (as a final coalgebra) to 2 (or to N, the codomain Toby spoke of) in the topos of sheaves on R. Toby, what is it? Vaughan Pratt PS. None of this contradicts the point you (PTJ) and Freyd have been making, since around 2002 apparently, concerning the constructive merits of apartness as an implementation of the glue used in the Freyd coalgebra, which I only very belatedly came to appreciate, namely within the past two days. In view of this I retract my "The choice of poisons is therefore manual glue vs. double induction" of last Wednesday. I am willing to believe that the Freyd coalgebra with manual glue implemented via apartness produces the "real reals" in these toposes of sheaves, but would like eventually to understand why of course. That said, I would still like to know whether our final coalgebra, for FX = N x X where x is "lexicographic product" suitably defined for an NNO N in a topos, is or is not equally real in these toposes. If it is then this would be a situation where apartness is not needed to produce the reals constructively, presumably contradicting Brouwer. From rrosebru@mta.ca Wed Feb 11 09:40:49 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 09:40:49 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFKX-00033v-FC for categories-list@mta.ca; Wed, 11 Feb 2009 09:40:45 -0400 MIME-Version: 1.0 Date: Tue, 10 Feb 2009 13:05:26 -0800 Subject: categories: Re: "Kantor dust" From: Greg Meredith To: "Prof. Peter Johnstone" , categories@mta.ca Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Greg Meredith Message-Id: Status: O X-Status: X-Keywords: X-UID: 30 Categorically minded, Many thanks for an interesting thread! Just out of curiousity, is the Conway construction clearly identified with the Dedekind reals? How does the construction fit into the constructivist debate? Best wishes, --greg On Mon, Feb 9, 2009 at 2:47 PM, Prof. Peter Johnstone < P.T.Johnstone@dpmms.cam.ac.uk> wrote: > On Mon, 9 Feb 2009, Dusko Pavlovic wrote: > > QUESTION 1: re peter johnstone's >> >> > > 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. >>> >> >> are you claiming that this statement is true with respect to every base >> topos >> and every real line in it? (the discussion seems to have touched upon the >> various constructions of the various real lines. it would be nice to know >> where is the one, over which you build the topos, is coming from.) >> >> That's actually a quote from Toby Bartels, not from me. > It's a statement about a topos built over the classical topos of sets; > the argument is a rather ad hoc one, and I'm not sure to what extent > it's possible to make it constructive. However, as I said elsewhere, I > prefer to work with the gros topos of spaces (i.e. sheaves on a suitable > full subcategory of spaces for the coverage consisting of jointly- > surjective families of open inclusions) and there it's quite clear > what you need: namely, Heine--Borel (equivalently, exponentiability > of R in your category of spaces). That's not true in all toposes; > you could try to get round it by basing your gros topos on locales > rather than spaces (the locale of formal reals being constructively > locally compact), but it's not clear (to me, at least) what the > result would actually mean if you based yourself on a topos where > the formal reals aren't spatial. > > QUESTION 2: is there a branch of constructivism that would reject as >> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as >> the >> coefficients of continued fractions? >> >> I don't think there is any doubt that the map exists. The problem is > that, > for most if not all schools of constructivism, it's wildly non-surjective. > > Peter Johnstone > > > > -- L.G. Meredith Managing Partner Biosimilarity LLC 806 55th St NE Seattle, WA 98105 +1 206.650.3740 http://biosimilarity.blogspot.com From rrosebru@mta.ca Wed Feb 11 09:41:43 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 09:41:43 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFLP-0003A9-Qf for categories-list@mta.ca; Wed, 11 Feb 2009 09:41:39 -0400 Date: Tue, 10 Feb 2009 22:18:41 +0000 (GMT) From: "Prof. Peter Johnstone" To: Greg Meredith , categories@mta.ca Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Prof. Peter Johnstone" Message-Id: Status: O X-Status: X-Keywords: X-UID: 31 On Tue, 10 Feb 2009, Greg Meredith wrote: > Categorically minded, > > Many thanks for an interesting thread! Just out of curiousity, is the Conway > construction clearly identified with the Dedekind reals? How does the > construction fit into the constructivist debate? > > Best wishes, > > --greg > The trouble with the Conway construction is not that it's non- constructive, but that it isn't (in any reasonable sense) a construction of the reals. If you stop it at the point when it finally constructs the real numbers 1/3, \sqrt{2}, \pi and so on, then it has also succeeded in constructing lots of non-real numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how do you distinguish the numbers you want from the ones you don't? I did, in both my first Topos Theory book and the Elephant, borrow Conway's recursive definition of multiplication to give a constructively valid definition of multiplication for Dedekind reals. I'm not aware of anyone else who has done that; but it seems to me the only intellectually respectable way to do it. Peter Johnstone From rrosebru@mta.ca Wed Feb 11 09:42:23 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 09:42:23 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFM2-0003FA-RV for categories-list@mta.ca; Wed, 11 Feb 2009 09:42:18 -0400 Date: Tue, 10 Feb 2009 16:13:51 -0800 From: Toby Bartels To: categories list Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 32 Steve Stevenson wrote in part: >Toby Bartels wrote: >>Floating-point reals have terrible theoretical properties; >>they're not even a ring (not even classically). >>This is why even after all of Kahan's good work on algorithms, >>rounding errors are unavoidable (the "Table-Maker's Dilemma"). >Being left-handed and old, I'll propose in my dotage that we may be >asking the wrong question. In a rewording, what constructive real >numbers are there for the purpose of >1. Being a model of an axiomatic characterization of the reals. >2 Being usable in supercomputing to compute values needed for modeling >and simulation. I would distinguish two slightly different purposes: 1. Being usable in principle to compute values 2. Being usable in practice to compute values needed for modeling, etc. And I'd say that constructive mathematics is inherently about (1), although often (and like even classical mathematics, usually best when) with an eye towards (2). But (2) itself is something different (applied mathematics, to give it a name; numerical analysis straddles these.) Although I've redefined them, I think that this remains true: >Number 1 requires that we have nice theoretical properties. Number 2 >requires something that is bounded only the dollars and life span. Those >interested in either purpose have (presumedly) a solution for >themselves. Interval arithmetic, despite being more complicated than arithemetic with either floating-point reals or Dedekind/Cauchy/whatever reals, is an interesting subject that promises to satisfy both (1)&(2). This is good for both: good for (1) on the general grounds that applied mathematics usually leads to good pure mathematics (especially, but not only, when that mathematics is constructive); and good for (2) since you'll have theorems that you can be sure of. >I'm willing to >live with a demonstrably correct approximation given that we are in an >uncertain world. Right, and interval arithmetic promises to get us such approximations. There's still the question of whether demonstrably correct ones are actually calculable in practice; that depends on the application. At some point, you have to go beyond even interval arithmetic and start dealing with probability distributions as your values, which is yet more complicated theoretically but matches yet more closely what one actually has in applications. I'm not sure how much this has to do with category theory anymore, but as interval arithmetic is already stretching my expertise, I don't think that I have much more to say anyway. --Toby From rrosebru@mta.ca Wed Feb 11 09:43:04 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 09:43:04 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFMg-0003Je-65 for categories-list@mta.ca; Wed, 11 Feb 2009 09:42:58 -0400 Date: Tue, 10 Feb 2009 21:49:35 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: "Kantor dust" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 33 Apropos of my > PS. [...] That said, I would > still like to know whether our final coalgebra, for FX = N x X where x > is "lexicographic product" suitably defined for an NNO N in a topos, is > or is not equally real in these toposes. If it is then this would be a > situation where apartness is not needed to produce the reals > constructively, presumably contradicting Brouwer. I returned to this question after a pleasant dinner this evening with Sol Feferman, Paul Eklof, and Grisha Mints, and it occurred to me almost immediately (my subconscious must have been working on it without my permission) that in a topos over any sufficient category of topological spaces (not that I have the faintest idea how to make that rigorous), it must be the case that the final coalgebra for the functor F described above is the "real reals." The intuitition behind this is that N together with an upper bound thereon (call it oo) has only two possible T0 topologies whose specialization order is the standard linear one, namely the Alexandroff and Scott topologies. These differ by a single open set, which is present in the former and absent from the latter. In the former it isolates oo from N, in the latter its absence allows oo to link up with N in the sense that every ultimately constant function on N must map oo to the limiting value of that function. There is a unique map from the Alexandroff to the Scott topology on this set preserving the NNO structure, and no map back (where would you send the Alexandroff open witnessing the solitude of oo?). So in any competition for a final coalgebra Scott is going to beat Alexandroff. Now in N^N as a representation of the isomorphism [0,oo) ~ [0,1)[1,2)[2,3)..., the objection that will naturally be raised to any claim that this could be the continuum is that, even though [0,1)[1,2) *looks* like it should glue together seamlessly, its implementation in terms of continued fractions will create a gap between [0,1) and [1,2) that is not found in the "real reals". While this gap cannot be used in the topos Set to distinguish N^N from the Freyd coalgebra, where things are so discrete that all realizations of the reals suffer from gaps, in a more topologically sensitive topos it becomes possible to find open sets willing to testify to these gaps in those cases where insufficient care has been taken to bump off these witnesses, as surely happens when one defines N^N naively as simply an exponential. Implementing the glue of the Freyd coalgebra via apartness bumps off all such witnesses to the disconnectedness of the Freyd continuum, making it thus far the sole survivor in this competition to define the reals constructively. (If there is another why isn't it in the Elephant?) In any topos with sufficiently accommodating open sets as to permit this Alexandroff-Scott distinction (surely not a tall order given that only one open set need be removed to pass from Alexandroff to Scott), I claim that the final coalgebra for the functor Dusko and I exhibited in our CMCS'99 paper bumps off the Alexandroff open witnessing a gap between [0,1) and [1,2), where the 1 in [1,2) plays the role of oo in my earlier discussion of N and oo. If the topos of sheaves on R, or on whichever essentially small version of Top Peter Johnstone prefers over R itself, does not result in removing this open set in a way that leaves no other witnesses to disconnectedness then I will be bitterly disappointed. If it does however then we have what as far as I'm aware must be the first alternative since Brouwer to apartness in formulating the continuum to the constructive standards set by toposophers. And moreover using much older technology than the Freyd coalgebra, namely good old continuous fractions (done right of course, none of this antimonotone 1/(1+x) stuff totally disconnecting them). (How old? Continued fractions are ancient, appearing in Euclid and no doubt going back a lot further as with much of Euclidean mathematics. They are a very natural and convenient way of representing reals, though with subtleties to trip one up, just as with the Freyd coalgebra.) Similar reasoning should also rehabilitate the constructivity of binary fractions, where the final coalgebra surely deletes the open set separating 0111... from 1000... Perhaps ASD has something to say about this---Paul? Vaughan Pratt From rrosebru@mta.ca Wed Feb 11 09:43:47 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 09:43:47 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFNN-0003O9-IK for categories-list@mta.ca; Wed, 11 Feb 2009 09:43:41 -0400 Date: Wed, 11 Feb 2009 01:01:28 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: "Kantor dust" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 34 Prof. Peter Johnstone wrote on Feb. 7 at 17:18 GMT: > 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. I had always been somewhat dissatisfied intuitively by the idea of excluding sequences of the form 01111.... It seemed more natural to identify them with those of the form 10000.... However I just assumed that these were equivalent approaches. Your point about making x < 1/2 decidable is a good one. I'm now convinced that it is better to identify than delete. Identification can be accomplished spatially, but perhaps it is more elegant to do so localically, namely by removing the open set that separates the two halves to be glued together. In a T0 space, doing so will identify the points anyway. However in the situation [0,1)[1,2) of my previous messages where there is no point on the left adjacent to the point 1 on the right, identification of points is not an option. The only remaining concern then is whether there's an open set separating [0,1) and [1,2). Finality should eliminate spurious open sets that have no reason to stick around. Vaughan From rrosebru@mta.ca Wed Feb 11 09:45:18 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 09:45:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFOr-0003bY-4r for categories-list@mta.ca; Wed, 11 Feb 2009 09:45:13 -0400 Date: Wed, 11 Feb 2009 01:01:28 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: "Kantor dust" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 35 Prof. Peter Johnstone wrote on Feb. 7 at 17:18 GMT: > 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. I had always been somewhat dissatisfied intuitively by the idea of excluding sequences of the form 01111.... It seemed more natural to identify them with those of the form 10000.... However I just assumed that these were equivalent approaches. Your point about making x < 1/2 decidable is a good one. I'm now convinced that it is better to identify than delete. Identification can be accomplished spatially, but perhaps it is more elegant to do so localically, namely by removing the open set that separates the two halves to be glued together. In a T0 space, doing so will identify the points anyway. However in the situation [0,1)[1,2) of my previous messages where there is no point on the left adjacent to the point 1 on the right, identification of points is not an option. The only remaining concern then is whether there's an open set separating [0,1) and [1,2). Finality should eliminate spurious open sets that have no reason to stick around. Vaughan From rrosebru@mta.ca Wed Feb 11 09:45:51 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 09:45:51 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFPP-0003gm-EN for categories-list@mta.ca; Wed, 11 Feb 2009 09:45:47 -0400 Date: Wed, 11 Feb 2009 12:55:48 +0000 From: Alexander Kurz MIME-Version: 1.0 To: categories Subject: categories: TACL 2009: Second Announcement and Call for Contributions Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Alexander Kurz Message-Id: Status: O X-Status: X-Keywords: X-UID: 36 =============================================================================== TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2009) =============================================================================== 7-11 July 2009 Institute for Logic, Language and Computation University of Amsterdam the Netherlands http://www.illc.uva.nl/tacl09/ Scope ----- Studying logics via semantics is a well-established and very active branch of mathematical logic, with many applications, in computer science and elsewhere. The area is characterized by results, tools and techniques stemming from various fields, including universal algebra, topology, category theory, order, and model theory. The program of the conference TACL 2009 will focus on three interconnecting mathematical themes central to the semantical study of logics and their applications: algebraic, categorical, and topological methods. This is the fourth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL). Earlier installments of this conference have been organized in Tbilisi (2003), Barcelona (2005), and Oxford (2007). Invited speakers -------------------------- Martin Hyland, University of Cambridge, United Kingdom Achim Jung, University of Birmingham, United Kingdom Vincenzo Marra, University of Milano, Italy Paul-Andre Mellies, University of Paris 7, France Ieke Moerdijk, University of Utrecht, Netherlands Ales Pultr, Charles University, Prague, Czech Republic Lutz Schroeder, University of Bremen, Germany Kazushige Terui, Kyoto University, Japan Constantine Tsinakis, Vanderbilt University, USA Featured topics --------------- Contributed talks can deal with any topic falling under the scope of the meeting. This includes, but is not limited to, the following areas: * Algebraic logic * Coalgebraic semantics * Categorical methods in logic * Domain theory * Fuzzy and many-valued logics * Lattices with operators * Modal logics * Non-classical logics * Ordered topological spaces * Ordered algebraic structures * Pointfree topology * Residuated structures * Stone-type dualities * Substructural logics * Topological semantics of modal logic Submissions ----------- Contributed presentations will be of two types: 20 minutes long presentations in parallel sessions and featured, 30 minutes long, plenary presentations. The submission of an abstract of 1-4 pages is required to be selected for a contributed presentation of either kind. While preference will be given to new work, results that have already been published or presented elsewhere will also be considered. More information on the submission procedure is available on the conference website. Grants ------------- TACL 2009 hopes to support junior and/or low budget participants whose contributed talk proposal has been approved from the PC. This support will take the form of fee waivers and of travel or accommodation grants. For more information, please visit the conference website. The deadline for grant application is April 22, 2009. Important dates --------------- March 15, 2009: Abstract submission deadline April 15, 2009: Notification of authors April 22, 2009: Grant application deadline July 7-11, 2009: Conference Program Committee ----------------- Guram Bezhanishvili, New Mexico State University, USA Nick Bezhanishvili, Imperial College London, United Kingdom Nick Galatos, University of Denver, USA Mai Gehrke, Radboud Universiteit, Nijmegen, Netherlands (Chair) Rob Goldblatt, Victoria University, Wellington, New Zealand Rosalie Iemhoff, University of Utrecht, Netherlands Ramon Jansana, University of Barcelona, Spain Alexander Kurz, University of Leicester, United Kingdom Franco Montagna, University of Siena, Italy Drew Moshier, Chapman University, USA Hiroakira Ono, Japan Advanced Institute of Science and Technology, Japan Yde Venema, Universiteit van Amsterdam, Netherlands Steve Vickers, University of Birmingham, United Kingdom Michael Zakharyaschev, Birkbeck, Universty of London, United Kingdom More Information ---------------- If you have any queries please send them to the conference email address: tacl09@uva.nl =============================================================================== From rrosebru@mta.ca Wed Feb 11 21:39:38 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 21:39:38 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXQWS-0004pf-Tj for categories-list@mta.ca; Wed, 11 Feb 2009 21:37:48 -0400 Date: Wed, 11 Feb 2009 11:55:49 -0400 (AST) From: Toby Kenney To: Vaughan Pratt , Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Kenney Message-Id: Status: O X-Status: X-Keywords: X-UID: 37 On Tue, 10 Feb 2009, Vaughan Pratt wrote: > As a (surely constructive!) witness to the surjectivity, indeed > bijectivity, of R, define the inverse S: [0,oo) --> N^N of R as > follows. (R converts sequences to Reals, which S turns back into > Sequences.) > > S(x)(0) = floor(x) > S(x)(n+1) = S(g(x mod 1))(n) > > where x mod 1 = x - floor(x) and g(x) = x/(1-x) : [0,1) --> [0,oo) is > the inverse of f(x) = x/(1+x) : [0,oo) --> [0,1) used in the definition > of R. > The trouble with this is that the floor function isn't constructive - the question "is x<2" is undecidable in the reals, but decidable in the natural numbers. The problem with the obvious definition: "Take the set of natural numbers below x, and take the join of this set." is that the natural numbers don't have K~-finite joins, only K-finite ones. Incidentally, has anyone looked at semilattices with K~-finite joins? (Or whatever your favourite notion of finiteness is.) Is there any use for something like the completion of N under K~-finite joins, other than allowing us to define the floor function? Toby From rrosebru@mta.ca Wed Feb 11 21:48:58 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 21:48:58 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXQh2-0005TW-QP for categories-list@mta.ca; Wed, 11 Feb 2009 21:48:44 -0400 MIME-Version: 1.0 Date: Wed, 11 Feb 2009 10:11:44 -0600 Subject: categories: Re: "Kantor dust" From: Michael Shulman To: "Prof. Peter Johnstone" , categories@mta.ca Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Michael Shulman Message-Id: Status: O X-Status: X-Keywords: X-UID: 38 On Tue, Feb 10, 2009 at 4:18 PM, Prof. Peter Johnstone wrote: >> Many thanks for an interesting thread! Just out of curiousity, is >> the Conway construction clearly identified with the Dedekind reals? >> How does the construction fit into the constructivist debate? > > The trouble with the Conway construction is not that it's non- > constructive, but that it isn't (in any reasonable sense) a > construction of the reals. If you stop it at the point when it > finally constructs the real numbers 1/3, \sqrt{2}, \pi and so > on, then it has also succeeded in constructing lots of non-real > numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how > do you distinguish the numbers you want from the ones you don't? And it isn't just "infinite" and "infinitesimal" numbers like \omega and 1/\omega that come along for the ride, either. Classically, the copy of the natural numbers sitting inside the surreal numbers is actually the *finite ordinal numbers*, and constructively there are many more ordinal numbers below \omega than there are natural numbers. For instance, { 0 | P } where P is an undecidable statement, is a perfectly good ordinal number that lies "somewhere between 0 and 1." Mike From rrosebru@mta.ca Wed Feb 11 21:49:37 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 21:49:37 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXQhn-0005WM-0K for categories-list@mta.ca; Wed, 11 Feb 2009 21:49:31 -0400 Date: Wed, 11 Feb 2009 17:33:59 +0000 (GMT) From: "Prof. Peter Johnstone" To: Vaughan Pratt , Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Prof. Peter Johnstone" Message-Id: Status: O X-Status: X-Keywords: X-UID: 39 On Tue, 10 Feb 2009, Vaughan Pratt wrote: > Apropos of my > >> PS. [...] That said, I would >> still like to know whether our final coalgebra, for FX = N x X where x >> is "lexicographic product" suitably defined for an NNO N in a topos, is >> or is not equally real in these toposes. If it is then this would be a >> situation where apartness is not needed to produce the reals >> constructively, presumably contradicting Brouwer. > > I returned to this question after a pleasant dinner this evening with > Sol Feferman, Paul Eklof, and Grisha Mints, and it occurred to me almost > immediately (my subconscious must have been working on it without my > permission) that in a topos over any sufficient category of topological > spaces (not that I have the faintest idea how to make that rigorous), it > must be the case that the final coalgebra for the functor F described > above is the "real reals." > Whoa! This simply can't work. Whatever the final coalgebra for N x (-) looks like, it must (thanks to Lambek) be isomorphic to N x itself, and therefore (since equality for N is decidable) must have lots of complemented subobjects {0} x itself, {1} x itself, ... The point of the continuity theorem for functions R --> R is that there are toposes in which R has *no* nontrivial complemented subobjects -- indeed, in which the sentence (\forall S : PR)((\forall x : R)((x \in S) \vee \neg(x\in S)) \implies ((S = R)\vee (S = \emptyset))) is valid. This is purely a matter of logic: it has nothing to do with the order, topological or any other sort of structure carried by the final coalgebra. So invoking Alexandroff and Scott isn't going to help at all. The only way to get round it (apart from using glue) is to replace N by some "nonstandard natural number object" having no nontrivial complemented subobjects -- but where you get that from, I don't know. Peter From rrosebru@mta.ca Wed Feb 11 21:50:16 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 21:50:16 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXQiR-0005ZQ-Ux for categories-list@mta.ca; Wed, 11 Feb 2009 21:50:11 -0400 Date: Wed, 11 Feb 2009 09:53:44 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: "Kantor dust" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 40 Vaughan Pratt wrote: > Similar reasoning should also rehabilitate the constructivity of binary > fractions, where the final coalgebra surely deletes the open set > separating 0111... from 1000... Perhaps ASD has something to say about > this---Paul? Unfortunately the reasoning is not similar enough to make this work. The crucial difference is that in the representation of [0,oo) ~ [0,1)[1,2)[2,3)... as N^N, there is no largest element of [0,1) whence the Scott topology omits the open set separating [0,1) from [1,0). With binary fractions however we have two points 0111... and 1000... with nothing between them and the inequality 0111... < 1000..., which the Scott topology must respect by preserving the open set separating them. There is (as far as I'm aware) no such localic alternative of the kind I was envisaging to either omitting 0111... or identifying it with 1000..., both of which are intrinsically spatial solutions to the problem of converting Cantor space 2^N to the continuum. In contrast the Alexandroff-to-Scott conversion of N^N to the continuum is localic in character, in that it operates on open sets instead of points. The crucial difference between classical and sheaf-theoretic toposes is that localic procedures are meaningless in the former. The latter permit the finer distinctions to be drawn that are needed to explicate constructivity, starting with the distinction between not-not and identity. (Unlike some other buggy posts of mine that I've been able to retract before Bob forwarded them to the list, this one went through too promptly for me to catch it in time. I made this mistake by incorrectly visualizing the gap between 0111... and 1000... as though it were the gap between .0 < .01 < .011 < .0111 < ... and ... < .1000 < .100 < .10 < .1 This makes no sense (a) because the finite sequences on the right should all be identified and (b) there are no finite sequences to begin with, the binary fractions are properly understood as infinite sequences, namely maps N --> 2. The paragraph was an afterthought I tacked on with insufficient consideration before posting.) Vaughan Pratt From rrosebru@mta.ca Wed Feb 11 21:51:46 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 21:51:46 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXQju-0005g3-B0 for categories-list@mta.ca; Wed, 11 Feb 2009 21:51:42 -0400 MIME-Version: 1.0 Date: Wed, 11 Feb 2009 11:56:40 -0800 Subject: categories: Re: "Kantor dust" From: Greg Meredith To: "Prof. Peter Johnstone" , categories@mta.ca Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Greg Meredith Message-Id: Status: O X-Status: X-Keywords: X-UID: 41 Dr Johnstone, Many thanks for the response. A couple of years ago, i did come up with a scheme for sifting through the widgets generated by the Conway construction. There's a one-liner translation of the Conway construction into a reflective process calculus [1]. Then, using the type schemes devised by Luis Caires , you can use behavioral types -- in principle -- to sort through the gadgets the Conway construction generates. This idea shares much of the spirit of the work done by Mads Dam on proof systems for the pi-calculus in his examples of logical specifications of process models of the naturals -- though to the best of my knowledge he never applied his ideas to the Conway construction. i cooked up this hair-brained idea in search of a more natural typing of a notion of quantity that is grounded in a conception of computing that i know how to reduce to practice. Best wishes, --greg [1] i'm ignoring a bunch of issues about which domain you use to solve the domain equations that present the reflective process calculus -- which impact how wide your summations and parallel compositions can be, which impact how wide the left and right side of the Conway games can be. But, therein lies at least on connection to category theory. Be that as i may, here is the 1-liner translation [| G |] = \Sigma_{G^L} @ [| G^L |] ?(x)(*x | [| G^L |]) | \Sigma_{G^R} @ [| G^R |]!( [| G^L |] ) The syntax of the reflective calculus that is the target of this translation is given below P,Q ::= 0 | x?A | x!C | *x | P+Q A ::= (y1,...,yN)P, C ::= (P1,...,PN) x,y ::= @P See the link above for a brief account of the calculus and a corresponding logic. i should note that the translation is horrifically inefficient and it was wading through the different optimizations -- while preserving nice compositional properties of the translation so that the definitions and proofs given by Conway easily port over through the translation to natural operations on the process models -- that sapped my motivation. On Tue, Feb 10, 2009 at 2:18 PM, Prof. Peter Johnstone < P.T.Johnstone@dpmms.cam.ac.uk> wrote: > On Tue, 10 Feb 2009, Greg Meredith wrote: > > Categorically minded, >> >> Many thanks for an interesting thread! Just out of curiousity, is the >> Conway >> construction clearly identified with the Dedekind reals? How does the >> construction fit into the constructivist debate? >> >> Best wishes, >> >> --greg >> >> The trouble with the Conway construction is not that it's non- > constructive, but that it isn't (in any reasonable sense) a > construction of the reals. If you stop it at the point when it > finally constructs the real numbers 1/3, \sqrt{2}, \pi and so > on, then it has also succeeded in constructing lots of non-real > numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how > do you distinguish the numbers you want from the ones you don't? > > I did, in both my first Topos Theory book and the Elephant, borrow > Conway's recursive definition of multiplication to give a > constructively valid definition of multiplication for Dedekind reals. > I'm not aware of anyone else who has done that; but it seems to > me the only intellectually respectable way to do it. > > Peter Johnstone > From rrosebru@mta.ca Wed Feb 11 21:52:38 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 21:52:38 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXQkl-0005ko-Dn for categories-list@mta.ca; Wed, 11 Feb 2009 21:52:35 -0400 From: "Bhupinder Singh Anand" To: "'Paul Taylor'" , Subject: categories: Re: "Kantor dust" Date: Thu, 12 Feb 2009 03:46:00 +0530 MIME-Version: 1.0 Content-Type: text/plain;charset="US-ASCII" Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: "Bhupinder Singh Anand" Message-Id: Status: O X-Status: X-Keywords: X-UID: 42 On Sunday, February 08, 2009 8:33 PM, Paul Taylor wrote in Categories: " ... people should be clear about WHICH OF MANY "CONSTRUCTIVE" THEORIES OF MATHEMATICS they mean as the context of their comments. ... If you want to construct Cantor space from the reals by the "missing third" construction, I would think that it makes little difference whether you start from Cauchy or Dedekind." Actually, there seem to be two issues involved here. The minor of the two: that the "missing third" construction yields a 'limit', namely the "Kantor dust"; The other: whether we can agree on any 'constructive' concept at all, such as, say, the standard interpretation of first-order Peano Arithmetic. As to the first: Consider an equilateral triangle ABC of height h and side s. Divide the base AC in half and construct two isosceles triangles of height h.d and base s/2, where 1>d>0. Iterate the construction on each constructed triangle ad infinitum. If the "Kantor dust" is a legitimate (fractal) set, then this construction, too, should yield a limiting configuration. Since the height of the constructed triangles at the n'th construction is h(d^n), and 1>d>0, it would seem that the base AC of the original equilateral triangle will always be the limiting configuration of the opposing sides. This is indeed so if 1/2>d>0, since the total length of the opposing sides is a Cauchy sequence whose limiting value is, indeed, the length s of the base AC. However, if d=1/2, the total length of all the sides opposing their base on AC is always 2s! Moreover, if d>1/2, the total length of all the sides opposing their base on AC is a monotonically increasing value. (To give it a practical flavour, let s be one light-year, and consider how long it would take a light signal to travel from A to C along the sides opposing the base in each of the above cases; and whether it makes any sense to assert that all the cases must have a limiting configuration.) So, whatever it is that the "missing third" construction is supposed to yield, it certainly cannot have any relation to the terms "third", "construction", "limit" and "set" under any interpretation of these terms that we normally conceive of in mathematics. The issue - as Thoralf Skolem emphasised in "Some remarks on axiomatized set theory", delivered in an address before the Fifth Congress of Scandinavian Mathematicians in Helsinki, 4-7 August 1922, with respect to the the Axiom of Choice - is that set-theory admits statements that are essentially non-verifiable under any conceivable interpretation; statements, moreover, which do not express any definable content and cannot, therefore, be expected to communicate any meaningful information unambiguously under interpretation: "So long as we are on purely axiomatic ground there is, of course, nothing special to be remarked concerning the principle of choice (though, as a matter of fact, new sets are not generated univocally by applications of this axiom); but if many mathematicians---indeed, I believe, most of them---do not want to accept the principle of choice, it is because they do not have an axiomatic conception of set theory at all. They think of sets as given by specification of arbitrary collections; but then they also demand that every set be definable. We can, after all, ask: What does it mean for a set to exist if it can perhaps never be defined? It seems clear that this existence can be only a manner of speaking, which can lead only to purely formal propositions---perhaps made up of very beautiful words---about objects called sets. But most mathematicians want mathematics to deal, ultimately, with performable computing operations and not to consist of formal propositions about objects called this or that." That the problem lies deeper - in fact at the very core of our fundamental assumptions - is seen if we note that our logical thinking is universally founded upon the validity of Aristotle's particularisation. This holds that an assertion such as, 'There exists an x such that F(x) holds'---usually denoted symbolically by '(Ex)F(x)'---can be validly inferred in the classical logic of predicates from the assertion, 'It is not the case that, for any given x, F(x) does not hold'---usually denoted symbolically by '~(Ax)~F(x)'. Now, in his 1927 address, Hilbert reviewed in detail his axiomatisation of classical Aristotlean predicate logic as a formal first-order epsilon-predicate calculus, in which he used a primitive choice-function symbol, 'epsilon', for defining the quantifiers 'for all' and 'exists'. In an earlier address "On The Infinite", delivered in Munster on 4th June 1925 at a meeting of the Westphalian Mathematical Society, Hilbert had shown that the formalisation proposed by him would adequately express Aristotle's logic of predicates if the epsilon-function was interpreted to yield Aristotlean particularisation. This, as Hilbert remarked in his 1927 address, was what he had set out to achieve as part of his 'proof theory': "... The fundamental idea of my proof theory is none other than than to describe the activity of our understanding, to make a protocol of the rules according to which our thinking actually proceeds." What came to be known later as Hilbert's Program---which was built upon Hilbert's 'proof theory'---can be viewed as, essentially, the subsequent attempt to show that the formalisation was also necessary for communicating Aristotle's logic of predicates effectively and unambiguously under any interpretation of the formalisation. This goal is implicit in Hilbert's remarks: "Mathematics in a certain sense develops into a tribunal of arbitration, a supreme court that will decide questions of principle---and on such a concrete basis that universal agreement must be attainable and all assertions can be verified." "... a theory by its very nature is such that we do not need to fall back upon intuition or meaning in the midst of some argument." The difficulty in attaining this goal constructively along the lines desired by Hilbert---in the sense of the above quotes---lies in the fact that, as Rudolf Carnap emphasised in a 1962 paper, "On the use of Hilbert's epsilon-operator in scientific theories", the Axiom of Choice is formally derivable as a theorem in a set theory ZF_epsilon, which is, essentially, Zermelo-Fraenkel set theory where the quantifiers are defined in terms of Hilbert's epsilon-function. The significance of this lies in the accepted interpretation of Paul Cohen's argument in his 1963-64 papers; they are primarily taken as definitively establishing that the Axiom of Choice is independent of a set theory such as ZF. Now, Cohen's argument---in common with the arguments of many important theorems in standard texts on the foundations of mathematics and logic---appeals to Aristotle's particularisation when interpreting the existential axioms of ZF (or statements about ZF ordinals) in the application of the seemingly paradoxical (downwards) Lowenheim-Skolem Theorem for legitimising putative models of a language (such as the standard model 'M' of ZF, and its forced derivative 'N', in Cohen's argument). Thus, Cohen's argument should really be taken to establish that, not only is Aristotle's particularisation 'stronger' than the Axiom of Choice, but that there is no sound interpretation of ZF that can appeal to Aristotle's particularisation. Moreover, the larger significance of Hilbert's formalisation of Aristotle's particularisation is that---in formal languages that prefer the more familiar '[A]' - as in '[(Ax)]' - as a primitive symbol to Hilbert's more logical choice function 'epsilon'---it implicitly gives formal legitimacy to Alfred Tarski's standard definitions of the satisfaction, and truth, of the formulas of a formal language under an interpretation, since these definitions faithfully mirror the particular interpretation of Hilbert's formalisation that appeals to Aristotle's particularisation. The reason: Under Tarski's definitions, the formally defined logical constant '[E]' in an occurrence such as '[(Ex)]'---which is formally defined in terms of the primitive (undefined) logical constant '[Ax]' as '[~(Ax)~ ...]'---always appeals to an interpretation such as 'There is some x such that ...' in any formal first-order mathematical language. In other words, Tarski's definitions ensure that, if the first-order predicate calculus of a first-order mathematical language admits quantification, then any putative model of the language must interpret existential quantification as Aristotle's particularisation. Selecting such a strong interpretation---i.e., one which favours Aristotle's particularisation---for the standard interpretation, say S, of the formal Peano Arithmetic PA has significant consequences. For instance, if we accept the logical validity of such interpretation, then S is sound (i.e., every PA-theorem interprets as true under S. Further, if S is sound, then PA is omega-consistent (i.e., we cannot have a PA-formula [F(x)] such that [F(n)] is PA-provable for any given PA-numeral [n], and [~(Ax)F(x)] is also PA-provable). Now, in his seminal 1931 paper, Godel showed that if a Peano Arithmetic such as his formal system P is omega-consistent, then it is incomplete, in the sense that he could constructively define a P-formula [R(x)] such that neither [(Ax)R(x)] nor [~(Ax)R(x)] are P-provable. However, he also showed in this paper that if P is consistent and [(Ax)R(x)] is assumed P-provable, then [~(Ax)R(x)] is P-provable. By Godel's definition of P-provability, it follows that there is a finite sequence [F_1], ..., [F_n] of P-formulas such that [F_1] is [Ax)R(x)], [F_n] is [~(Ax)R(x)], and, for 2=< i =< n, [F_i] is either a P-axiom or a logical consequence of the preceding formulas in the sequence by the rules of inference of P. Now, a proof sequence of P necessarily interprets as a sound deduction sequence under any sound interpretation of P. It follows that we cannot have a sound interpretation of P under which [(Ax)R(x)] interprets as true and [~(Ax)R(x)] as false. Since both [(Ax)R(x)] and [~(Ax)R(x)] are closed P-formulas, it follows that the P-formula [(Ax)R(x) => ~(Ax)R(x)] interprets as true under every sound interpretation of P. By Godel's completeness theorem, [(Ax)R(x) => ~(Ax)R(x)] is, therefore, P-provable; whence [~(Ax)R(x)] is P-provable. Since Godel also showed that, if P is consistent, then [R(n)] is P-provable for any given P-numeral [n], it follows that P is not omega-consistent. Since Godel's argument holds in PA, we further have that the standard interpretation S of PA is not sound; moreover, no sound interpretation of PA can appeal to Aristotle's particularisation! Thus the difficulty in agreeing upon the concept of a 'constructive' theory is deep-rooted in our dependence on Aristotle's logic of predicates which, whilst allowing us the luxury of expressing the most subjectively conceived of our abstract concepts not only in languages of common discourse such as English, but also in mathematical languages such as ZF, is inadequate for ensuring that that which we express in the most basic of our mathmatical languages, namely Peano Arithmetic, can be communicated effectively and unambiguously. That a sound interpretation of Peano Arithmetic exists - moreover, one that allows us to communicate effectively and unambiguously - is indicated by the fact that we unhesitatingly entrust our lives each moment of each day to mechanical and electronic artefacts whose reliability is essentially founded on the ability of PA to admit unambiguous and effective communication. Accordingly, in a recently arXived paper (link below), I consider a weakened, finitary, interpretation B (of an omega-inconsistent PA) which avoids appealing to Aristotlean particularisation in the interpretation of the existential quantifier, and which is actually implicit in Turing's 1936 analysis of computable functions. This is the interpretation B of PA obtained if, in Tarski's inductive definitions---of the satisfaction and truth of the formulas of PA under the 'standard' interpretation S of PA---we apply Occam's razor and weaken the definition of subjective Tarskian satisfiability by replacing it with an algorithmically verifiable definition of objective Turing-satisfiability. Not only is the interpretation sound, but it implies that PA is categorical; we can thus, in principle, communicate perfectly with technologically advanced extra-terrestrial intelligences. http://arxiv.org/PS_cache/arxiv/pdf/0902/0902.1064v3.pdf Regards, Bhup From rrosebru@mta.ca Wed Feb 11 21:53:17 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 11 Feb 2009 21:53:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXQlN-0005oB-Eg for categories-list@mta.ca; Wed, 11 Feb 2009 21:53:13 -0400 Date: Wed, 11 Feb 2009 15:51:06 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: Categories mailing list Subject: categories: Re: "Kantor dust" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 43 Prof. Peter Johnstone wrote: > Whoa! This simply can't work. Whatever the final coalgebra for N x (-) > looks like, it must (thanks to Lambek) be isomorphic to N x itself, > and therefore (since equality for N is decidable) must have lots of > complemented subobjects {0} x itself, {1} x itself, ... The point of > the continuity theorem for functions R --> R is that there are toposes > in which R has *no* nontrivial complemented subobjects [...] > The only way to get round it (apart from using glue) > is to replace N by some "nonstandard natural number object" having no > nontrivial complemented subobjects -- but where you get that from, I > don't know. You're assuming product distributes over sums, which would be true for ordinary product but I specified lexicographic product, with the left argument as the "high order digit" (converse of the usual convention for ordinal product in ordinal arithmetic). Why should {0} x N be a complemented subobject of N x N when lexicographic product attaches the "end" of it to {1} x {0} , which I would expect it will in a topos of sheaves when participating in a final coalgebra for N x X. Vaughan From rrosebru@mta.ca Thu Feb 12 22:09:32 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Feb 2009 22:09:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXnRU-0000GI-UJ for categories-list@mta.ca; Thu, 12 Feb 2009 22:06:12 -0400 MIME-Version: 1.0 Subject: categories: Fields Workshop on Smooth Structures - Accommodation Date: Wed, 11 Feb 2009 22:29:01 -0500 From: "Pieter Hofstra" To: Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: "Pieter Hofstra" Message-Id: Status: O X-Status: X-Keywords: X-UID: 44 Fields Workshop on Smooth Structures in Logic, Category Theory and = Physics=20 May 1-3 2008, Ottawa *** Since the weekend of the Workshop coincides with the annual Tulip = Festival (which attracts many tourists) it will be difficult and = expensive to find accommodation in town. We have therefore reserved = rooms at two nearby hotels (at a discount rate) as well as a few units = in the University Residence. We can hold these rooms until April 1st, so = we recommend those who intend to attend the workshop to book as soon as = possible in order to avoid disappointment. Information about these = hotels can be found on the local web page: http://aix1.uottawa.ca/~scpsg/Fields09/Fields09.smoothworkshop.html Best regards, R. Blute P. Hofstra P. Scott M. Warren From rrosebru@mta.ca Thu Feb 12 22:09:32 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Feb 2009 22:09:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXnSB-0000Ix-5J for categories-list@mta.ca; Thu, 12 Feb 2009 22:06:55 -0400 Date: Wed, 11 Feb 2009 20:05:50 -0800 From: Toby Bartels To: categories list Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 45 Vaughan Pratt wrote in part: >Toby Bartels claims it's obvious, in which case there should be a short >construction of a nonconstant function from N^N (as a final coalgebra) >to 2 (or to N, the codomain Toby spoke of) in the topos of sheaves on R. > Toby, what is it? An element s of N^N as a final coalgebra of X |-> N x X decomposes into an element s0 of N and an element s+ of N^N. In this notation, the easiest of the desired functions is s |-> s0. Other functions N^N -> N include s |-> s+0, s++0, ...; there are more. This can be done in any topos (actually in more categories than that). If any of these is constant, then N is a terminal object, so if it's an NNO (as it should be to justify the notation N^N) we are in the terminal category (the inconsistent topos). --Toby Bartels From rrosebru@mta.ca Thu Feb 12 22:09:32 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Feb 2009 22:09:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXnTL-0000Nn-6h for categories-list@mta.ca; Thu, 12 Feb 2009 22:08:07 -0400 Date: Wed, 11 Feb 2009 20:25:25 -0800 From: Toby Bartels To: categories@mta.ca Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 46 Dusko Pavlovic wrote in part: [Prof. Johnstone responded to most of this, but I want to address one point.] >there are >many things that need to be computed with the reals, and no one >representation fits for all purposes. so the statement >>nobody uses the binary reals >probably has more counterexamples than, say, the statement "nobody >uses toposes". even if "the" binary reals were completely wrong. What I meant is that no practising constructivist accepts that the binary reals are the (or a) good notion of real number, especially since no practising constructivist believes they form a ring. I don't intend this as a dogamatic statement, and I'd be very interested to here of any exceptions, but nevertheless I believe that it is true. I certainly don't mean that nobody, not even a constructivist, uses the binary reals as an approximation to real numbers for the purposes of convenient calculations. And of course, classical mathematicians do believe that the binary reals are (all of) the reals. As I suggested in a reply to Steve Stevenson, constructive mathematics is about what can in principle be computed exactly. What can in practice be computed closely enough is another question, quite a useful one to ask but not at all the same thing. (And what can in practice be computed exactly is another good question, one that I'm interested in but don't know enough about.) --Toby From rrosebru@mta.ca Thu Feb 12 22:09:32 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Feb 2009 22:09:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXnSi-0000Ku-Od for categories-list@mta.ca; Thu, 12 Feb 2009 22:07:28 -0400 Date: Wed, 11 Feb 2009 20:10:47 -0800 From: Toby Bartels To: categories@mta.ca Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 47 Prof. Peter Johnstone wrote in part: >The trouble with the Conway construction is not that it's non- >constructive, but that it isn't (in any reasonable sense) a >construction of the reals. If you stop it at the point when it >finally constructs the real numbers 1/3, \sqrt{2}, \pi and so >on, then it has also succeeded in constructing lots of non-real >numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how >do you distinguish the numbers you want from the ones you don't? Can you get anywhere by imposing (at that stage) some Archimedean conditions? We need to know first how to interpret natural numbers as Conway numbers, then take the subset of those x such that -n < x < n for some n, and identify x and y if -1 < (x-y)n < 1 for every n. --Toby From rrosebru@mta.ca Thu Feb 12 22:10:28 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Feb 2009 22:10:28 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXnU8-0000Qq-4F for categories-list@mta.ca; Thu, 12 Feb 2009 22:08:56 -0400 Date: Thu, 12 Feb 2009 09:00:58 +0000 (GMT) From: "Prof. Peter Johnstone" To: Vaughan Pratt , Subject: categories: Re: "Kantor dust" MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Prof. Peter Johnstone" Message-Id: Status: O X-Status: X-Keywords: X-UID: 48 On Wed, 11 Feb 2009, Vaughan Pratt wrote: > Prof. Peter Johnstone wrote: >> Whoa! This simply can't work. Whatever the final coalgebra for N x (-) >> looks like, it must (thanks to Lambek) be isomorphic to N x itself, >> and therefore (since equality for N is decidable) must have lots of >> complemented subobjects {0} x itself, {1} x itself, ... The point of >> the continuity theorem for functions R --> R is that there are toposes >> in which R has *no* nontrivial complemented subobjects [...] >> The only way to get round it (apart from using glue) >> is to replace N by some "nonstandard natural number object" having no >> nontrivial complemented subobjects -- but where you get that from, I >> don't know. > > You're assuming product distributes over sums, which would be true for > ordinary product but I specified lexicographic product, with the left > argument as the "high order digit" (converse of the usual convention for > ordinal product in ordinal arithmetic). For goodness' sake, Vaughan! How many times do I have to tell you that I'm talking about *the underlying object* of the final coalgebra, and not its order structure or its topology? If the underlying object of the lexicographic product is the ordinary (cartesian) product -- and if it's not, then I don't know what it is -- then it distributes over sums because that's what products do in a topos. > Why should {0} x N be a > complemented subobject of N x N when lexicographic product attaches the > "end" of it to {1} x {0} , which I would expect it will in a topos of > sheaves when participating in a final coalgebra for N x X. > The order structure can't do any sort of "attaching" that negates the complementedness of the underlying subobject, and neither can the topology. The only thing that can do that is to make identifications between endpoints -- i.e. to use "glue" a la Freyd. Peter From rrosebru@mta.ca Thu Feb 12 22:10:57 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Feb 2009 22:10:57 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXnUu-0000Td-EH for categories-list@mta.ca; Thu, 12 Feb 2009 22:09:44 -0400 From: Bas Spitters To: "Galchin, Vasili" Subject: categories: Re: "Kantor dust" Date: Thu, 12 Feb 2009 10:05:10 +0100 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Bas Spitters Message-Id: Status: RO X-Status: X-Keywords: X-UID: 49 Let me use this as an excuse to advertise the work of Russell O'Connor, who is about to complete a PhD in Nijmegen working with me. O'Connor's project was to implement exact real numbers in type theory in a machine verified way. His implementation is fairly efficient and completely verified in the Coq proof assistant. Real numbers are implemented using (a variant of) Cauchy sequences. He used the completion monad on metric spaces to write a Haskell-style "effectful" functional program in Coq (http://arxiv.org/abs/cs/0605058). He combined the same monad with the list monad to obtain an implementation of compact sets (pictures, graphs, i.e. Cantor set). http://arxiv.org/abs/0806.3209 Together we implemented the Riemann integral by combining the step function monad with the completion monad: http://arxiv.org/abs/0809.1552 It was very pleasant to see how much category theory pops up naturally when one tries to implement exact real numbers in a certified way. To come back to your question: there is a *certified implementation* of compact sets of the plane. Cantor set is an example of this. O'Connor's paper includes much more discussion than what I would like to repeat here. I recommend it. Bas On Friday 30 January 2009 08:18:39 Galchin, Vasili wrote: > [Note from moderator: this may have been sent incorrectly earlier, > apologies if you have received it twice.] > > Dear Category group, > > Here is a definition of Cantor dust .... > http://en.wikipedia.org/wiki/Cantor_set. > > My question is from a constructivist viewpoint does this set really > exist and if so, why? > > Very kind regards, > > Vasili From rrosebru@mta.ca Thu Feb 12 22:12:39 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Feb 2009 22:12:39 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXnWQ-0000bX-Fe for categories-list@mta.ca; Thu, 12 Feb 2009 22:11:18 -0400 Mime-Version: 1.0 (Apple Message framework v624) Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=US-ASCII; format=flowed To: Categories list From: Paul Taylor Subject: categories: Dedekind versus Cauchy reals Date: Thu, 12 Feb 2009 12:54:07 +0000 Sender: categories@mta.ca Precedence: bulk Reply-To: Paul Taylor Message-Id: Status: O X-Status: X-Keywords: X-UID: 50 I wanted to reply to what Toby Bartells and Thomas Streicher said in response to my challenge to say why Cauchy sequences are often preferred to Dedekind cuts as constructions of the real line. However, I made the mistake of trying to read through the whole thread, so I'm afraid this posting has ended up in a somewhat rambling state. Also, I shall postpone the discussion of why DEDEKIND reals are good for COMPUTATION to another posting. NOTE TO ANYONE READING THIS IN AN ARCHIVE: There have been numerous very interesting contributions to this thread from Toby Bartels, Giovanni Curi, Peter Johnstone, Dusko Pavlovic, Vaughan Pratt, Steve Stevenson and others, but many of them have been posted under Subject: lines including the words Kantor dust This is an excellent thread, though unfortunately on the wrong mailing list. But I know that Peter Schuster reads "categories", so maybe he will chip in from the point of view of Bishop's constructive analysis. Some quick answers to various people's questions first. When I have spoken about "CONSTRUCTIONS" of the real line or of Cantor space, I mean the word in the usual non-formal mathematical sense, not according to any doctrine of constructivity. Even in a particular system, I don't think it makes sense to say whether the "construction" of a SPACE takes finite time. We can ask such questions (and, in more detail, about "complexity") for computations of INTEGERS FROM INTEGERS. Some people, in particular some of those who take part in "Computability and Complexity in Analysis", claim that this question is meaningful for REAL NUMBERS. But for OBJECTS, I don't see that it has any clear meaning. Toby Bartels said that the "UNDERLYING-SET AXIOM" in ASD is impredicative. This is correct, but I introduced this axiom as a "straw man". First, in order to say exactly what is needed to make ASD equivalent to (locally compact locales over) an elementary topos. Second, to make the point that a great deal of mainstream mathematics is computable and does NOT require underlying sets. I see the main thread of ASD as being about a computable theory. Toby has also said a lot of interesting things about many different systems. These illustrate my point that it is essential to state which system, or which notion of "constructivity" you intend. He has said, for example * The Dedekind reals can also be constructed in CZF (Peter Aczel's predicative constructive set theory) even if you remove countable choice, using subset collection aka fullness. * Similarly, if you remove identity types from intensional type theory (so breaking the justification of countable choice), you can still justify the fullness axiom and so construct the Dedekind reals (albeit not literally as sets of rational numbers). * The Cauchy reals exist an a Pi-W-pretopos (equivalently, in a constructive set or type theory with exponentiation but no power sets or even fullness and with infinity but no countable choice). * But the Dedekind reals, as far as [he] can tell, do not; excluded middle, power sets, fullness, or countable choice would each do the job, but you need ~something~. I would challenge someone to consider the last of these questions seriously, maybe taking a hint from the second. ASD provides another, as it uses lambda term over a special object instead of talking about "sets" of rational numbers. Peter Johnstone, on the other hand, has referred to the fact that both constructions exist in the topos-theoretic context, and are in general different. I don't want to put words into Peter's mouth, but a lot of evidence from "ordinary mathematics" says that the Dedekind reals are preferable. Giovanni Curi has also described the situation in several settings, apparently coming down on the side of Dedekind. (I am citing other people's postings primarily in order to encourage readers to read throught the thread.) The reason why we need to be clear about the different systems is that the mathematical results are DIFFERENT in them, in INTERESTING ways. It is very easy to adopt the habit of taking a particular system as given, and then asserting or denying that some theorem is "constructive", as a judgement about the THEOREM. However, they are typically headline results from mainstream mathematics, so it is the SYSTEM and not the theorem that is under scrutiny. In particular, I would like to turn the tables on the predicativists. A lot of excellent mathematics has been done in Martin-Lof type theory. More recently, certain categorists have been inspired by this to study "Pi-W-pretoposes" (which surely deserve a better name). But these theories pick a few items from the (by Godel's theorem, inexhaustible) collection of possible type-forming operations. Two questions naturally arise: * Why do you consider that the axioms that you have chosen are legitimate? * Why stop with them? For example, the recent debate amongst various constructive disciplines has shown that it is valuable to set down explicit rules about WHICH JOINS one may legitimately form in the lattice of open subspaces of a space: * In locale theory, one can form "all" of them, or, from a more constructive point of view, "enough" of them to obtain right adjoints such as Heyting implication and the direct image f_*. * In ASD, the indexing objects of legitimate joins are called OVERT. You can take this as a tautologous definition, in which case the notion of "overtness" is variable and might, for example, be extended by introducing ORACLES. * In Formal Topology, the ability to form unions is governed by Martin-Lof Type Theory, wherein the "sets" (over which we may form unions) are closed under implication. (At least, I believe that this is the case - no doubt someone will correct me if not.) From a computational point of view, this is a questionable thing to do (hence my first question). * Algebraic Set Theory has an axiomatisation based on the properties of OPEN MAPS. The latter are the same as families of overt spaces, in the same way that proper maps are families of compact spaces. Various workers on AST have augmented these axioms, explicitly with the purpose of including different LOGICAL connectives. So why not consider the TYPE OF DEDEKIND REALS too? This is a perfectly serious suggestion, and indeed it is precisely what Andrej Bauer and I have been doing. Dedekind completeness is a rule for INTRODUCING real numbers, given pairs of predicates, whilst the Heine--Borel theorem introduces quantified predicates. See www.PaulTaylor.EU/ASD/analysis.html for a summary of this SYNTACTIC theory, along with the papers that develop it. I intend to answer Thomas Streicher's "pragmatic" reasons for computing with Cauchy sequences in a separate posting, but I'd like to pick out the "foundational" part here: > AC_N of course allows you to magically find a modulus of convergence > for every Cauchy sequence. But like Church's Thesis or Brouwer's > Theorem this is sort of a Deus ex machina (actually those are 2 > contradictory dei ex machina!) and thus of moderate help for exact > computation on the reals. (Do you see what I mean by "heresy"?) The alleged conflict between Church's Thesis and Brouwer's Theorem (I would prefer to say the Heine--Borel theorem) is in fact exactly the point at which Andrej Bauer and I began our collaboration, in November 2004. He asked me whether I believed both of these things, which I said I did, and he progressively took me through the construction of the Kleene Tree -- to the point of contradiction. Of course, I wasn't going to accept that, so we back-tracked, and in particular I set out what I meant by Church's thesis. I think this formulation is in Pino Rosolini's thesis, and it is proved for ASD in "Scott domains in ASD" (rejected by CTCS 2002). There is a map p:N->Sigma^N that is "universal" in the (weak) sense that, for any map f:N->Sigma^N, there is some (not necessarily unique) fill-in q:N->N with f=p.q: > N . | . |p q. | . | . V . f V N---------> Sigma^N I forget how the conversation with Andrej went on from that point, but shortly afterwards he wrote down the Dedekind cut for the supremum of a non-empty compact overt subspace of R. Our construction of R took off from there. This "conflict between Church's Thesis and Brouwer's Theorem" illustrates another important principle about the methodology of mathematics: COUNTEREXAMPLES CLOSE MINDS When someone demonstrates a counterexample, what they legitimately prove is typically D, E, F |- not G. Then they assert "not E", after which an entire discipline gets built on the failure of E. Cantor's theorem about the non-isomorphism of a set with its powerset is perhaps the dominant example of this. This is an "argument by authority", one of the principal fallacies of logic. For one thing, D, E, F and G play symmetrical roles in the argument, so why pick on E as the erroneous assumption? Eventually, some heretic comes along and points out that this proof makes other assumptions A, B and C. By substituting different ideas, A', B' and C', they manage to show that these and D, E, F and G can validly co-exist. However, because of the pernicious influence of the counterexample on other people's minds, it is very difficult for the new ideas to get a hearing. Finally, a footnote about CONWAY'S NUMBERS. As Peter Johnstone has already pointed out, these include the ordinals. However, the traditional theory of the ordinals depends VERY HEAVILY on excluded middle. The intuitionistic theory is therefore rather complicated and, in particular, there are several different kinds of intuitionistic ordinals, for which see "Intuitionistic Sets and Ordinals" by Paul Taylor, JSL 61 (1996). "Algebraic Set Theory" by Andre Joyal and Ieke Moerdijk, CUP 1996? and my web page www.PaulTaylor.EU/ordinals/. This means that the intuitionistic version of Conway numbers would be even more complicated, although Frank Rosemeier made a start in "A Constructive Approach to Conway's Theory of Games" in "Reuniting the Antipodes: Constructive and Nonstandard Views of the Continuum}, Peter Schuster, Ulrich Berger and Horst Osswald (eds), Springer-Verlag, 2001. There are further remarks on the interaction amongst Dedekind completeness, the Archimedean property and Conway's numbers at the end of section 12 of "The Dedekind reals in ASD". Paul Taylor From rrosebru@mta.ca Thu Feb 12 22:12:55 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 12 Feb 2009 22:12:55 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXnX2-0000fe-Lh for categories-list@mta.ca; Thu, 12 Feb 2009 22:11:56 -0400 MIME-Version: 1.0 Date: Fri, 13 Feb 2009 01:07:08 +0100 Subject: categories: Re: Dedekind versus Cauchy reals From: Andrej Bauer To: categories@mta.ca, Thomas Streicher Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Andrej Bauer Message-Id: Status: O X-Status: X-Keywords: X-UID: 51 This is a reply to Thomas's post about "Dedekind vs. Cauchy". I am too young to know why Cauchy reals were preferred by the early constructivists, so I will reply only to remarks that regard real-number computation, of which I have more experience. Thomas gives pragmatic reasons for preferring Cauchy sequences, actually the rapid ones, with rate of convergence 2^-n. Given a rapid Cauchy sequence we can easily get an approximation to any desired degree. On the other hand, Thomas says, a Dedekind real is implemented as a semidecision procedure, which forces us to _guess_ approximations to the real. And he says this must be done in parallel, which just makes things worse. Firstly, I think arguments which are based too heavily on efficiency are on a shaky ground. C is faster than Haskell, therefore everyone should use C. Perhaps nobody has rally tried to implement efficient Dedekind reals so how can we tell? In fact, as far as I know, nobody has until last year. By the way, Cauchy sequences with a fixed rate of convergence are a bad idea if you worry about efficiency. As Norbert Mueller has demonstrated over the years, it is better to allow Cauchy sequences (actually sequences of eventually shrinking intervals) _without_ a priori conditions on the rate of convergence. Somewhat paradoxically, by allowing arbitrarily slow rate of convergence we are able to write _faster_ real arithmetic. This is a non-obvious fact which the practitioners have been trying to get across, but it's not sticking with the theorists for some reason. Thomas's argument about AC_N being of only moderate help is true, but in a twisted way: in practice AC_N is just never used explicitly, and moduli of continuity, even fixed ones like 2^-n, are avoided at all cost. Secondly, there are other criteria by which we should judge an implementation. One of them is expressivity and the level of abstraction. With the Dedekind reals certain concepts are more easily expressed. For example, if one wants to talk constructively about compactness of the closed interval, Cauchy reals will not be of much help (unless you essentially declare [0,1] to be compact), whereas locale-theoretic constructions in the style of Dedekind will work better. Lastly, since my computer believes in number choice, there really is no dilemma. The Cauchy and Dedekind reals _must_ be equivalent to the computer. Paul Taylor and I have devised algorithms for efficient, sequential computation with Dedekind reals which use the equivalence with Cauchy reals under the hood (at least I think that's what is going on, but I do not fully understand the whole thing yet). There is no need to think of a Dedekind real as a clumsy semidecision procedure. Instead, the left and the right cut may be seen as instructions for calculating better approximations from existing ones. This can be done quite efficiently with Newton's method (the variant for interval arithmetic). The computation that comes out then behaves very much like an iterative procedure for computing a Cauchy sequence. Best regards, Andrej From rrosebru@mta.ca Fri Feb 13 13:47:07 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 13 Feb 2009 13:47:07 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LY27G-0000nb-LW for categories-list@mta.ca; Fri, 13 Feb 2009 13:46:18 -0400 Date: Thu, 12 Feb 2009 21:40:48 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: "Kantor dust" Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 52 Toby Bartels wrote: > Prof. Peter Johnstone wrote in part: > >> The trouble with the Conway construction is not that it's non- >> constructive, but that it isn't (in any reasonable sense) a >> construction of the reals. If you stop it at the point when it >> finally constructs the real numbers 1/3, \sqrt{2}, \pi and so >> on, then it has also succeeded in constructing lots of non-real >> numbers like \omega, 1/\omega, 1/2-1/\omega and so on. So how >> do you distinguish the numbers you want from the ones you don't? > > Can you get anywhere by imposing (at that stage) some Archimedean conditions? > We need to know first how to interpret natural numbers as Conway numbers, > then take the subset of those x such that -n < x < n for some n, > and identify x and y if -1 < (x-y)n < 1 for every n. Pretty much. Peter was speaking of day \omega. With your identification applied to that day, the only other step needed is to remove \omega and -\omega and then you have exactly the field R. A more uniform way of arriving at R is to take the subset consisting of those numbers expressible as a nonempty proper sup or nonempty proper inf in an even number of ways. This is because at day \omega you have \omega, -\omega, D \cdot 3 in the sense of ordinal product, where D is the set of dyadic rationals and 3 = {-1/omega < 0 < 1/omega} (the range of adjustments to each dyadic rational), and the dyadic irrationals. \omega is a proper sup of the integers but not a nonempty inf (though it is the empty inf), and dually for -\omega. The dyadic rationals are not a proper sup or inf of anything (their increments on either side prevent this) but the increment on the left is a proper sup but not a proper inf, and dually on the right. The dyadic irrationals are both a proper sup of what's below them and a proper inf of what's above them. Puzzle. Bearing in mind that on all days prior to day \omega, every number satisfies this criterion, on what other days besides day \omega does this criterion produce a field? Vaughan From rrosebru@mta.ca Fri Feb 13 13:47:08 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 13 Feb 2009 13:47:08 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LY26c-0000jG-Fs for categories-list@mta.ca; Fri, 13 Feb 2009 13:45:38 -0400 Date: Thu, 12 Feb 2009 20:39:03 -0800 From: Toby Bartels To: Categories list Subject: categories: Re: Dedekind versus Cauchy reals MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: Toby Bartels Message-Id: Status: O X-Status: X-Keywords: X-UID: 53 Paul Taylor wrote in part: >Toby Bartels said that the "UNDERLYING-SET AXIOM" in ASD is impredicativ= e. >This is correct, but I introduced this axiom as a "straw man". >First, in order to say exactly what is needed to make ASD equivalent >to (locally compact locales over) an elementary topos. OK, that's pretty much what I thought. >Second, to make the point that a great deal of mainstream mathematics >is computable and does NOT require underlying sets. I see the main >thread of ASD as being about a computable theory. I hope you won't mind if I take this opportunity to ask something that I've been idly wondering about ASD lately, and which is related to this thread (even the Cantor set). That is: to what extent does ASD have inductive and coinductive objects; in other words: to what extent do polynomial functors have initial algebras and final (terminal) coalgebras? Of course, N is put in by hand as the initial algebra of X |-> 1 + X. And I know that you've constructed Cantor space as 2^N (through a bit of argument since exponentials don't always exist) and the proof that this is the final coalgebra of X |-> 2 x X goes throug= h. But the final coalgebra of X |-> N x X would be Baire space, which is not locally compact, so we don't expect that to work. My intuition is that polynomials with overt discrete coefficients should have overt discrete initial algebras, while those with compact Hausdorff coefficients should have compact Hausdorff final coalgebras. Have you any thoughts about that question? >[Toby] has said, for example >* [...] >* Similarly, if you remove identity types from intensional type theory > (so breaking the justification of countable choice), you can still > justify the fullness axiom and so construct the Dedekind reals > (albeit not literally as sets of rational numbers). >* [...] >* But the Dedekind reals, as far as [he] can tell, do not; excluded > middle, power sets, fullness, or countable choice would each do the > job, but you need ~something~. >I would challenge someone to consider the last of these questions >seriously, maybe taking a hint from the second. I'd be interested to hear if anybody has done ~any~ work on the second: intensional type theory without identity types. It seems to me to work if done in the style of Thierry Coquand (with inductive types and dependent products as the main constructions) but not if done in the style of Per Martin-L=C3=B6f (with W-types and dependent and finitary products and sums). I should probably say something about what categories would serve as syntactic models of such a type theory, but I never fully worked that out. --Toby From rrosebru@mta.ca Fri Feb 13 13:47:10 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 13 Feb 2009 13:47:10 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LY282-0000su-Lr for categories-list@mta.ca; Fri, 13 Feb 2009 13:47:06 -0400 From: Thomas Streicher Date: Fri, 13 Feb 2009 13:28:54 +0100 To: Andrej Bauer , categories@mta.ca Subject: categories: Re: Dedekind versus Cauchy reals MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Thomas Streicher Message-Id: Status: O X-Status: X-Keywords: X-UID: 54 Dear Andrej, wasn't aware of the fact that insisting on fixed rate of convergence can make things slower. My argument BTW was not about speed but rather about the ability to read off the desired result. In case of Cauchy sequences I need the modulus of convergence to know when I am close enough. In case of Dedekind reals that's not needed PROVIDED the left and the right set are given by enumerations of rationals. I "just" have to wait till close enough approximations from left and right have been enumerated. But is it right that in your implementation the left and right cuts are given by ENUMERATIONS of its elements and now via semidecision procedures? I guess so. Well, but when considering Dedekind cuts this way it essentially boils down to introducing reals as interval nestings (as done in High School sometimes). So really the question is whether Cauchy sequences or interval nestings are better. The way I interpret your remarks is that interval nesting is better since it allows one to avoid moduli of continuity which is good since fixed rate of convergence is a source of inefficiency. I think even constructivists refuting impredicativity have no problem to embrace representations by interval nestings. If I am not mistaken one finds this also in Martin-Loef's 1970 book. Thomas From rrosebru@mta.ca Fri Feb 13 13:47:42 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 13 Feb 2009 13:47:42 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LY28Z-0000xX-FY for categories-list@mta.ca; Fri, 13 Feb 2009 13:47:39 -0400 MIME-Version: 1.0 Date: Fri, 13 Feb 2009 14:47:57 +0100 Subject: categories: enriched Kan-extensions From: Tony Meman To: categories Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Tony Meman Message-Id: Status: O X-Status: X-Keywords: X-UID: 55 Dear category theorists, I have a question concerning enriched left Kan-extensions. My situation is the following: V is a complete and cocomplete symmetric monoidal closed category, A and B two small V categories and F:A-->B a V-functor. Via the V-left-Kan extension one gets a V-adjunction Lan_F: V-Fun(A,V)<-->V-Fun(B,V):F* where F* denotes the precomposition with F. Moreover, the V-category V-Fun(A,V) and the V-category V-Fun(B,V) are equipped with a symmetric V-monoidal structure respectively. Is it known, under which conditions the adjunction (Lan_F,F*) is actually a monoidal adjunction? Surely, it must have something to do with F: I suppose that F have to be a symmetric monoidal functor with respect to a symmetric V-monoidal structure on and A and B. The V-monoidal structures on A and B also should have something to do with the V-monoidal structure on V-Fun(A,V) and V-Fun(B,V). Does anyone know a reference for this situation? Thank you in advance for any help. Tony From rrosebru@mta.ca Fri Feb 13 13:48:21 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 13 Feb 2009 13:48:21 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LY29C-00012A-2C for categories-list@mta.ca; Fri, 13 Feb 2009 13:48:18 -0400 Date: Fri, 13 Feb 2009 16:05:14 +0100 From: gcuri@math.unipd.it To: categories@mta.ca Subject: categories: Re: Dedekind versus Cauchy reals MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: gcuri@math.unipd.it Message-Id: Status: O X-Status: X-Keywords: X-UID: 56 Quoting Paul Taylor : > > > Toby has also said a lot of interesting things about many different > systems. These illustrate my point that it is essential to state > which system, or which notion of "constructivity" you intend. > > He has said, for example > * The Dedekind reals can also be constructed in CZF (Peter Aczel's > predicative constructive set theory) even if you remove countable > choice, using subset collection aka fullness. > * Similarly, if you remove identity types from intensional type theory > (so breaking the justification of countable choice), you can still > justify the fullness axiom and so construct the Dedekind reals > (albeit not literally as sets of rational numbers). > * The Cauchy reals exist an a Pi-W-pretopos (equivalently, in a > constructive set or type theory with exponentiation but no power > sets or even fullness and with infinity but no countable choice). > * But the Dedekind reals, as far as [he] can tell, do not; excluded > middle, power sets, fullness, or countable choice would each do the > job, but you need ~something~. > > I would challenge someone to consider the last of these questions > seriously, maybe taking a hint from the second. ASD provides another, > as it uses lambda term over a special object instead of talking about > "sets" of rational numbers. A note concerning the possibility of constructing the Dedekind reals with= out fullness, etc: the Dedekind reals can be defined in constructive set theory even withou= t excluded middle, power sets, fullness, or countable choice. The point is = that they then form a class and not a set. Class-sized objects are however the norm in a constructive predicative se= tting. For instance, a (non-trivial) locale is carried by a class that is never = a set; in general a formal space or formal topology is a large object too, so th= at one often deals with superlarge "categories" with large homsets. Giovanni Curi Dipartimento di Matematica Pura ed Applicata Universita' degli Studi di Padova www.math.unipd.it From rrosebru@mta.ca Sun Feb 15 19:12:44 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Feb 2009 19:12:44 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LYq8y-0003pF-Iy for categories-list@mta.ca; Sun, 15 Feb 2009 19:11:24 -0400 From: "Ronnie Brown" To: "Categories list" Subject: categories: Re: Dedekind versus Cauchy reals Date: Sun, 15 Feb 2009 07:43:31 -0000 MIME-Version: 1.0 Content-Type: text/plain;format=flowed;charset="iso-8859-1";reply-type=original Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: "Ronnie Brown" Message-Id: Status: O X-Status: X-Keywords: X-UID: 57 I have enjoyed, without entirely following, the debate on this theme and would like to ask some naive questions. Rather practical toposes are presheaf toposes. Do the Dedekind and Cauchy reals differ in some of those? To be more practical again, one use of the reals is to analyse motion, as Lawvere has said. Motion includes change of data, which is analysed by statistics. But suppose the data to be analysed has structure, such as a directed graph. Then perhaps we need the reals in the topos of directed graphs? I.e. insert the required structure at the very beginning of the study, instead of post facto. Is the law of large numbers valid in the (??) probablity theory based on those reals? And which reals? Idle curiosity I fear! Ronnie From rrosebru@mta.ca Sun Feb 15 19:12:44 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Feb 2009 19:12:44 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LYq89-0003mW-QP for categories-list@mta.ca; Sun, 15 Feb 2009 19:10:33 -0400 Date: Sat, 14 Feb 2009 22:50:12 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories list Subject: categories: Re: Dedekind versus Cauchy reals Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 58 Andrej Bauer wrote: > There is > no need to think of a Dedekind real as a clumsy semidecision > procedure. Instead, the left and the right cut may be seen as > instructions for calculating better approximations from existing ones. > This can be done quite efficiently with Newton's method (the variant > for interval arithmetic). The computation that comes out then behaves > very much like an iterative procedure for computing a Cauchy sequence. If everything can be related to interval arithmetic in one way or another, why not take interval arithmetic itself as the gold standard for the constructive reals? The Edalat-Escardo-Potter domain-theoretic analysis of interval arithmetic struck me as sufficiently canonical that I don't understand why all the alternatives aren't being evaluated relative to that one. Are there alternatives that compensate for some shortcoming of interval arithmetic as understood through the lens of domain theory? Vaughan Pratt From rrosebru@mta.ca Sun Feb 15 19:12:44 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 15 Feb 2009 19:12:44 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LYq9t-0003s4-2N for categories-list@mta.ca; Sun, 15 Feb 2009 19:12:21 -0400 Date: Mon, 16 Feb 2009 09:31:43 +1100 Subject: categories: Re: enriched Kan-extensions From: Steve Lack To: Tony Meman ,categories Mime-version: 1.0 Content-type: text/plain; charset="US-ASCII" Content-transfer-encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Steve Lack Message-Id: Status: O X-Status: X-Keywords: X-UID: 59 Dear Tony, As you say, this depends on how the monoidal structures on the functor categories are defined. The only sensible way I know of which uses the given structures on A and B is by Day convolution, and then your result will hold if F itself is strong monoidal. See the Day-Street paper "Kan extensions along promonoidal functors" in volume 1 of TAC. Regards, Steve Lack. On 14/02/09 12:47 AM, "Tony Meman" wrote: > Dear category theorists, > I have a question concerning enriched left Kan-extensions. > > My situation is the following: > V is a complete and cocomplete symmetric monoidal closed category, A and B > two small V categories and F:A-->B a V-functor. Via the V-left-Kan extension > one gets a V-adjunction > Lan_F: V-Fun(A,V)<-->V-Fun(B,V):F* > where F* denotes the precomposition with F. > > Moreover, the V-category V-Fun(A,V) and the V-category V-Fun(B,V) are > equipped with a symmetric V-monoidal structure respectively. Is it known, > under which conditions the adjunction (Lan_F,F*) is actually a monoidal > adjunction? Surely, it must have something to do with F: I suppose that F > have to be a symmetric monoidal functor with respect to a symmetric > V-monoidal structure on and A and B. The V-monoidal structures on A and B > also should have something to do with the V-monoidal structure on V-Fun(A,V) > and V-Fun(B,V). > > Does anyone know a reference for this situation? > > Thank you in advance for any help. > Tony > > From rrosebru@mta.ca Wed Feb 18 03:23:17 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Feb 2009 03:23:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LZgl4-0003BT-BE for categories-list@mta.ca; Wed, 18 Feb 2009 03:22:14 -0400 Date: Mon, 16 Feb 2009 15:41:08 +0000 From: "Roy L. Crole" MIME-Version: 1.0 To: categories@mta.ca Subject: categories: 2nd Call for Participation - Midlands Graduate School in the Foundations of Computing Science 2009 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: "Roy L. Crole" Message-Id: Status: O X-Status: X-Keywords: X-UID: 60 Dear Colleagues, We still have a small number of places remaining at MGS2009, available at the full rate of =A3380. If you would like to attend, please complete = the registration form provided on the web page. **************************************************************** Midlands Graduate School in the Foundations of Computing Science **************************************************************** =20 30th March - 3rd April 2009 University of Leicester, UK http://www.cs.le.ac.uk/events/mgs2009 The 10th Midlands Graduate School (MGS) is taking place! WHAT IS MGS 2009? The MGS is an intensive course of lectures on the Foundations of Computing. It is very well established, with this being our 10th anniversary, and has always proved a very popular and successful event. This year we have Professor Peter Dybjer, Chalmers, Sweden, as guest lecturer. The lectures are aimed at graduate students, typically in their first or second year of study for a PhD. However, the school is open to anyone who is interested in learning more about mathematical computing foundations. We very much welcome international applications as well as from those from the UK. COURSES - Foundations Thorsten Altenkirch Category Theory =20 Paul Levy The Lambda Calculus =20 Henrik Nilsson Functional Programming =20 - Advanced Peter Dybjer Normalization by Evaluation =20 Martin Escardo Semantics =20 Nicola Gambino Dependent Types Alexander Kurz Coalgebra Uday Reddy Separation Logic Georg Struth Automated Theorem Proving WHERE IS MGS 2009? MGS 2009 will take place at John Foster Hall, University of Leicester, UK, with accommodation and lectures all on one site. Breakfasts, lunches and four course dinners will be provided. For further details and registration visit http://www.cs.le.ac.uk/events/mgs2009 Roy Crole and Daniela Petrisan. From rrosebru@mta.ca Wed Feb 18 03:23:17 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Feb 2009 03:23:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LZgjJ-00039g-6R for categories-list@mta.ca; Wed, 18 Feb 2009 03:20:25 -0400 MIME-Version: 1.0 Date: Mon, 16 Feb 2009 08:01:05 +0100 Subject: categories: Re: Dedekind versus Cauchy reals From: Andrej Bauer To: Vaughan Pratt , Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Andrej Bauer Message-Id: Status: O X-Status: X-Keywords: X-UID: 61 On Sun, Feb 15, 2009 at 7:50 AM, Vaughan Pratt wrote: > If everything can be related to interval arithmetic in one way or > another, why not take interval arithmetic itself as the gold standard > for the constructive reals? The Edalat-Escardo-Potter domain-theoretic > analysis of interval arithmetic struck me as sufficiently canonical that > I don't understand why all the alternatives aren't being evaluated > relative to that one. Are there alternatives that compensate for some > shortcoming of interval arithmetic as understood through the lens of > domain theory? I essentially agree with you, namely that interval arithmetic (actually, the interval domain) plays a fundamental role in the construction of reals, as well as in practical computation (the fastest implementations use interval arithmetic on top of multiple-precision floating point). A result of Vasco Brattka says that any two implementations of the structure of reals (arithmetic, abs, semidecidable <, limit operator for rapid sequences) are computably isomorphic. This can be interpreted as saying that the domain-theoretic reals are as good as any other version. One reason why this is not the end of the story is that we do not understand what happens at higher types. Vasco tells us that given two versions of reals, R1 and R2, they are computably isomorphic. But how about functions R1 -> R1, functionals (R1 -> R1) -> R1 and other higher types? For example, if R1 is the domain-theoretic reals (constructed as the maximal elements of the interval domain) and R2 is the "Cauchy reals" (represented as streams of digits, including negative digits), then we know that the hierachies R1, R1 -> R1, (R1 -> R1) -> R1, ... and R2, R2 -> R2, (R2 -> R2) -> R2, ... agree in the first three terms, but do not know what happens after that. This was established by Alex Simpson, Martin Escardo and myself. Dag Normann has also investigated the two hierarchies. For the familiar case of natural numbers John Longley has shown that "in nature" there are only three versions of the hierachy N, N -> N, (N -> N) -> N, ... These are the hereditarily effective operators, the Kleene-Kreisel continuous functionals, and a "mixed" version (the computable Kleene-Kreisel continuous functionals). We would like to have a result like that for reals, but we're stuck with the continuous version of the hierarchy at rank 3. In terms of implementation, the question is the following: does it matter whether the reals are implemented transparently (the programmer has access to their internal representation) or opaquely (reals are values of an abstract data type whose internal workings cannot be inspected)? We know that up to types of rank 2 it does not matter. Until such questions are answered, settling with a single construction or theory of real number computation is premature. By the way, can you give a single interesting _total_ functional of type ((R -> R) -> R) -> R? (Please don't ask me to define "interesting".) Andrej From rrosebru@mta.ca Wed Feb 18 03:23:30 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Feb 2009 03:23:30 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LZgmE-0003DQ-Rn for categories-list@mta.ca; Wed, 18 Feb 2009 03:23:26 -0400 Mime-Version: 1.0 (Apple Message framework v624) Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit From: Paul Taylor Subject: categories: Dedekind versus Cauchy reals Date: Mon, 16 Feb 2009 22:09:21 +0000 To: Categories list Sender: categories@mta.ca Precedence: bulk Reply-To: Paul Taylor Message-Id: Status: O X-Status: X-Keywords: X-UID: 62 Thomas Streicher said, in response to Andrej Bauer, > In case of Cauchy sequences I need the modulus of convergence to know > when I am close enough. In case of Dedekind reals that's not needed > PROVIDED the left and the right set are given by enumerations of > rationals. You still need a condition with the same objective. It is given by LOCATEDNESS: for any d I "just" have to wait till close enough approximations from left > and right have been enumerated. But is it right that in your > implementation the left and right cuts are given by ENUMERATIONS > of its elements and now via semidecision procedures? I guess so. > Well, but when considering Dedekind cuts this way it essentially > boils down to introducing reals as interval nestings (as done in > High School sometimes). No -- you're trying to force Dedekind cuts (and real computation in general) into the straitjacket of Cauchy sequences. This is part of the longstanding prejudice in favour of numbers and against logic. If you GENUINELY take Dedekind cuts on board, you can start thinking of computation using GEOMETRY and other disciplines. The fragment of the ASD calculus for R has a syntax with - types N, R, Sigma and Sigma^R - arithmetic operations + - * - arithmetic relations < > != - the usual stuff on N too - logical operations T F /\ \/ - existential quantifiers over N, R, open intervals, closed intervals (with real endpoints), ie with types Sigma^N-->Sigma etc - universal quantifiers over closed bounded intervals - definition by description for N - Dedekind cuts for R - primitive recursion over N at all types. The primitive calculation is therefore a LOGICAL question, - existentially or universally quantified over some ranges of the variables - of an arithmetic comparison ( > OR < ) - of two polynomials. This suggests using SEMI-ALGEBRAIC GEOMETRY, although I do not know enough about this subject to see how to use it. A quick way that answers a universally quantified question surprisingly often is just to evaluate the polynomials using interval (Moore) arithmetic. Another technique is to split the range of one of the variables. A much more powerful technique uses the INTERVAL Newton algorithm. The "classical" Newton algorithm DOUBLES THE NUMBER OF BITS OF PRECISION at each iteration -- once you have got below the "typical length" of the problem. Above this, it behaves chaotically. The interval Newton algorithm "knows" how to behave -- like interval halving when the problem is essentially combinatorial, and like the classical algorithm when we're below the typical length. Whereas UNIVERSALLY quantified questions can often be answered using "ordinary" (Moore) interval arithmetic, EXISTENTIAL ones are handled in a similar way, but using "back-to-front" intervals, whose arithmetic was originally formulaed by Edgar Kaucher. Andrej's program uses forward and backward intervals to evaluate Dedekind cuts, but does not at the moment use the interval Newton algorithm, Vaughan Pratt said, again in response to Andrej, > If everything can be related to interval arithmetic in one way or > another, why not take interval arithmetic itself as the gold standard > for the constructive reals? The Edalat-Escardo-Potter domain-theoretic > analysis of interval arithmetic struck me as sufficiently canonical > that > I don't understand why all the alternatives aren't being evaluated > relative to that one. Are there alternatives that compensate for some > shortcoming of interval arithmetic as understood through the lens of > domain theory? In previous ages, mathematicians of the day "standardised" on unit fractions or Roman numerals. At one conference that I attended, a whole afternoon was given over to a team of interval analysts who wanted to "standardise" their subject, in the bureaucratic sense of getting some document accepted by the ISO. One of the speakers did some dreadful mathematics that depended heavily on decidable choices, another presented some "software engineering" that was -- even for that subject -- dogmatic and outdated, whilst the third gave a (good) political speech. If you read what most interval analysts write, it is ad hoc and wrong-headed. There is, in particular, a fundamental error in regarding the interval [d,u] as the closed set of numbers BETWEEN d and u. Amongst other things, this makes it impossible to understand Kaucher arithmetic (back-to-front intervals). Another widespread belief is that interval arithmetic is some wonderful new algebraic system in the tradition of the complex numbers and quaternions. A much simpler way of understanding the interval [d,u], which is both constructive and compatible with Kaucher arithmetic, is as a DEDEKIND PSEUDO-CUT. The two halves consist of the numbers that are SO FAR KNOWN to be respectively less and greater than the number being calculated. This representation is much more natural, in that advancing calculation and the Scott topology are in the same sense as increasing the sets D and U, whereas the closed set [d,u] becomes smaller. Essentially, the two parts D and U then lead their own separate lives, each belonging to an "extended line" with the Scott topology. It's actually very simple. Paul Taylor PS. I have flagged Toby Bartels' question, > to what extent does ASD have inductive and coinductive objects, to answer after the current thread about the reals, Cantor space, the Conway numbers, constructivity and toposes has died down. PPS. My website has now gone live on a new server at www.PaulTaylor.EU whilst the old one is still at www.monad.me.uk. Please tell me about missing links and server errors. The "monad" address will become a redirection in a couple of weeks' time, and will be discontinued next year. From rrosebru@mta.ca Wed Feb 18 21:04:17 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Feb 2009 21:04:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LZxHo-0006bC-Lp for categories-list@mta.ca; Wed, 18 Feb 2009 21:01:08 -0400 Date: Wed, 18 Feb 2009 22:23:14 +0600 (NOVT) From: "Serge P. Kovalyov" To: categories@mta.ca Subject: categories: Question on E-coreflective subcategories MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Serge P. Kovalyov" Message-Id: Status: O X-Status: X-Keywords: X-UID: 63 Dear Category Theory gurus, In my reserach I have encountered the following problem. Let A be a full isomorphism-closed coreflective subcategory of a category C, G : C -> A be a coreflection. Let (E, M) be a factorization system for C-morphisms, such that class G(E) contains class of all A-isomorphisms and is contained in class of all A-retractions. Is any of the following statements correct: 1. If functor G preserves M, then it preserves E. 2. If any M-morphism is mono, then an M-morphism belongs to Mor(A) provided that its codomain belongs to Ob(A). Examples known to me satisfy both statements, but I fail to prove any. Thanks, Serge. From rrosebru@mta.ca Wed Feb 18 21:04:17 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 18 Feb 2009 21:04:17 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LZxIj-0006eM-Le for categories-list@mta.ca; Wed, 18 Feb 2009 21:02:05 -0400 From: Richard Moot To: Richard Moot Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit Subject: categories: ESSLLI 2009 Call for Participation Date: Wed, 18 Feb 2009 18:26:26 +0100 Sender: categories@mta.ca Precedence: bulk Reply-To: Richard Moot Message-Id: Status: O X-Status: X-Keywords: X-UID: 64 ====================================================================== = = = CALL FOR PARTICIPATION = = = = 21st EUROPEAN SUMMER SCHOOL IN LOGIC, LANGUAGE AND INFORMATION = = ESSLLI 2009 = = = = Bordeaux, July 20-31 2009 = = = ====================================================================== http://esslli2009.labri.fr/ The European Summer School in Logic, Language and Information (ESSLLI) is organized every year by the Association for Logic, Language and Information (FoLLI) in different sites around Europe. The main focus of ESSLLI is on the interface between linguistics, logic and computation. The 21st edition of ESSLLI will be held in Bordeaux, recently selected as a Unesco World Heritage site. * Course Program * ESSLLI offers a total of 48 courses and workshops, divided among foundational, introductory and advanced courses, and including a total of 7 workshops. The courses and workshops cover a wide variety of topics within the three areas of interest: Language and Computation, Language and Logic, and Logic and Computation. http://esslli2009.labri.fr/programme.php * Registration * Registration for ESSLLI is open. Early registration rates are 225 euros for students and 350 euros for others. Early registration deadline: 1st of May 2009. http://esslli2009.labri.fr/reg.php Richard Moot ESSLLI Organizing Committee From rrosebru@mta.ca Fri Feb 20 19:03:25 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 20 Feb 2009 19:03:25 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LaeM4-0004hy-TB for categories-list@mta.ca; Fri, 20 Feb 2009 19:00:25 -0400 Date: Thu, 19 Feb 2009 23:57:18 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Fixing the constructive continued-fraction definition of the reals: proofs and refutations Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 65 Prof. Peter Johnstone wrote: > On Wed, 11 Feb 2009, Vaughan Pratt wrote: > >> Prof. Peter Johnstone wrote: >>> Whoa! This simply can't work. Whatever the final coalgebra for N x (-) >>> looks like, it must (thanks to Lambek) be isomorphic to N x itself, >>> and therefore (since equality for N is decidable) must have lots of >>> complemented subobjects {0} x itself, {1} x itself, ... The point of >>> the continuity theorem for functions R --> R is that there are toposes >>> in which R has *no* nontrivial complemented subobjects [...] >>> The only way to get round it (apart from using glue) >>> is to replace N by some "nonstandard natural number object" having no >>> nontrivial complemented subobjects -- but where you get that from, I >>> don't know. >> >> You're assuming product distributes over sums, which would be true for >> ordinary product but I specified lexicographic product, with the left >> argument as the "high order digit" (converse of the usual convention for >> ordinal product in ordinal arithmetic). > > For goodness' sake, Vaughan! How many times do I have to tell you that > I'm talking about *the underlying object* of the final coalgebra, and > not its order structure or its topology? If the underlying object of > the lexicographic product is the ordinary (cartesian) product -- and > if it's not, then I don't know what it is -- then it distributes over > sums because that's what products do in a topos. Peter, if you don't mind my answering a question with a question, did either of us mention underlying objects before? (I could have overlooked an earlier message.) When you speak out of the blue about "the underlying object of the final coalgebra," what exactly is underlying what? I feel like I've abruptly stepped through a mirror into some strange part of topos theory that will be covered in Volume 3 of the Elephant. One notion of underlying object that makes sense for me in the context so far is the set E(1,X) of elements of an object X in a topos E. With this notion I have a prayer of making sense of your claim in the context of the following four objects of a topos E with NNO N (and whatever else if anything is needed to ensure that objects 2-4 exist in E). 1. N^2. 2. The initial object among all objects X with an element 0: 1 --> X and maps s,t: X --> X satisfying st = ts. 3. As for 2 with ts = t in place of st = ts. 4. As for 3 with st = s in place of ts = t. If I've grasped this slippery topos concept, all four objects X of E have, as their underlying set E(1,X), the set of all pairs (m,n) of natural numbers (up to isomorphism of course). In 2 the elements take the form of terms (s^m||t^n)(0) meaning m s's and n t's applied in any order to 0. In 3 the elements take the form of maps s^m(t^n(0)) meaning n applications of t (coarse tuning) followed by m applications of s (fine tuning), while in 4 they take the form of maps t^m(s^n(0)) (3 with s and t interchanged). I could well imagine 1 and 2 turning out to be isomorphic, but I feel I would get a lot from seeing the proof of whichever way that goes. I presume that 3 and 4 are isomorphic on the ground that s and t can be mapped to any two endomorphisms whence there must exist an isomorphism exchanging s and t. I imagine I would get less out of a rigorous proof of that unless there's a bug in the previous sentence. If there's no bug then this would seem to constitute a subtle difference from algebra, where the signature labels the operations in a way that prevents such an interchange and puts 3 and 4 in distinct albeit equivalent varieties. Whether or not 1 and 2 are isomorphic, they are in some sense both representations of the ordinary product of N with itself. Where I have greater difficulty is imagining an isomorphism between 2 and 3 merely on the ground that they have the same underlying object. I'm really not following your logic here. 2 implements product concurrently whereas 3 and 4 implement it sequentially. How could they be isomorphic in every topos? (I can see that they'd have to be isomorphic in Set, and presumably certain other toposes which however I have no idea how to characterize.) I regard 3 and 4 as equivalent definitions of the ordinal w^2 (w = \omega) in a topos. What are the necessary subobjects of 3, and which of those are necessarily complemented? I can think of the singletons {(m,n)}, the set of successor elements (since s: X --> X is a monic), and the *uniform* tails s^m: X --> X of the successor elements, but not the set of limit ordinals in w^2 since t: X --> X is not a monic, and hence not anything involving t. Are there other subobjects of 3, and can you characterize them all in some neat way? If as you seem to be implying, 1-4 are isomorphic, then I would have to agree with your "for goodness' sake" (yes it was really stupid of me not to see that) and resign myself to the absence (thus far) of any alternative to apartness for representing the reals. If however you agree with me that they can't be isomorphic (via something more reliable than my proof by agitated gesticulation born of summary dismissal) then we can move on with the rest of my envisaged program to define the continuum [0,x) in a topos without appealing to apartness. This too may or may not have bugs, whence the "proofs and refutations" qualification in the new subject line. (If this were darts there'd be a sequential scoreboard, concurrently with beer.) Vaughan From rrosebru@mta.ca Sun Feb 22 02:23:18 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 22 Feb 2009 02:23:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lb7hq-0005zo-Mq for categories-list@mta.ca; Sun, 22 Feb 2009 02:20:50 -0400 Date: Sat, 21 Feb 2009 12:29:48 -0400 (AST) Subject: categories: Re: Fixing the constructive continued-fraction definition of the reals: proofs and refutations From: "Toby Kenney" To: "Vaughan Pratt" , categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Sender: categories@mta.ca Precedence: bulk Reply-To: "Toby Kenney" Message-Id: Status: O X-Status: X-Keywords: X-UID: 66 Vaughan Pratt wrote in part: ... > > One notion of underlying object that makes sense for me in the context > so far is the set E(1,X) of elements of an object X in a topos E. With > this notion I have a prayer of making sense of your claim in the contex= t > of the following four objects of a topos E with NNO N (and whatever els= e > if anything is needed to ensure that objects 2-4 exist in E). > > 1. N^2. > > 2. The initial object among all objects X with an element 0: 1 --> X > and maps s,t: X --> X satisfying st =3D ts. > > 3. As for 2 with ts =3D t in place of st =3D ts. > > 4. As for 3 with st =3D s in place of ts =3D t. > ... > > I could well imagine 1 and 2 turning out to be isomorphic, but I feel I > would get a lot from seeing the proof of whichever way that goes. > > I presume that 3 and 4 are isomorphic on the ground that s and t can be > mapped to any two endomorphisms whence there must exist an isomorphism > exchanging s and t. I imagine I would get less out of a rigorous proof > of that unless there's a bug in the previous sentence. If there's no > bug then this would seem to constitute a subtle difference from algebra= , > where the signature labels the operations in a way that prevents such a= n > interchange and puts 3 and 4 in distinct albeit equivalent varieties. > > Whether or not 1 and 2 are isomorphic, they are in some sense both > representations of the ordinary product of N with itself. > > Where I have greater difficulty is imagining an isomorphism between 2 > and 3 merely on the ground that they have the same underlying object. > I'm really not following your logic here. 2 implements product > concurrently whereas 3 and 4 implement it sequentially. How could they > be isomorphic in every topos? (I can see that they'd have to be > isomorphic in Set, and presumably certain other toposes which however I > have no idea how to characterize.) I regard 3 and 4 as equivalent > definitions of the ordinal w^2 (w =3D \omega) in a topos. > I=B4m pretty sure the objects (1)-(4) are isomorphic. Here=B4s a sketch o= f the proof: Let X be the object (3), i.e. the initial object with a morphism 0:1---->= X and morphisms s:X---->X, t:X---->X with st=3Ds. Let Y be the object (2), i.e. the initial object with a morphism 0:1---->Y and morphisms u:Y---->Y= , v:Y---->Y. (1)&(2): We clearly have maps 0 x 0: 1----> N^2, succ x 1_N and 1_N x succ : N^2---->N^2, inducing the map Y---->N^2. For an element a of Y, we can form maps f_{t,a}: N---->Y by 0 ]----> a, succ ]----> t, and f_{s,a} by 0 ]---->a, succ ]----> s. We can now form a map N x N ----> Y by f(a,b)=3Df_{t,{f_{s,0}(a)}}(b). We can check that these maps form an isomorphism. (2)&(3): Lemma: X is a monoid We construct the addition X x X---->X by its exponential transpose X---->X^X. This is the map induced by 1_X:1---->X^X, s^X:X^X---->X^X, and t^X:X^X---->X^X. We think of this monoid structure as ordinary ordinal addition. We now construct morphisms s=B4 and t=B4 X---->X, given by s=B4(x)=3Dx + = 1 and t=B4(x)=3D\omega + x. It is clear that s=B4 and t=B4 commute. This induce= s a morphism Y---->X. On Y, we can create the projection map p:Y---->N as Y is isomorphic to N = x N. We also have the inclusion i : N ----> N x N given by a ]----> (a,0). Now ipu and v satisfy ipuv=3Dipu (ipu is the map \_ + \omega. This induce= s a map X ----> Y, which will be the inverse of the map Y ----> X. I will check the details later to make sure. But I would be very surprise= d if there were any problems. Toby From rrosebru@mta.ca Sun Feb 22 02:23:18 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 22 Feb 2009 02:23:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lb7jP-00062P-Nn for categories-list@mta.ca; Sun, 22 Feb 2009 02:22:27 -0400 Date: Sat, 21 Feb 2009 09:18:29 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Fixing the constructive continued-fraction definition of the reals: proofs and refutations Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 67 Toby Kenney wrote: > Vaughan Pratt wrote in part: >> I could well imagine 1 and 2 turning out to be isomorphic, but I feel I >> would get a lot from seeing the proof of whichever way that goes. Thanks very much, Toby. I didn't (and still don't) have any intuition into what objects and morphisms are present in the free topos with NNO, but your proof will help me fill in the gaps in this neighborhood of it. On the one hand there are lots of objects one can talk about in language analogous to that characterizing the NNO, on the other there are also lots of morphisms one can talk about that identify those objects (up to isomorphism), and I'm still at the very early stage of learning how to walk along that ridge line without falling off one side or the other. Joyal and Moerdijk, Algebraic Set Theory, show how to construct sup-semilattices with sups up to a specified size S. Obviously not every topos with NNO supports every S, but presumably S = K (Kuratowski-finite) is always present. Your proof if correct shows that ts = t is too strong. What if I relax it to ts <= t and proceed as in J&M to construct the initial such object? Can you still construct your isomorphism, or do we end up with a weaker relationship? If the latter then we should have t(0) >= t(s(0)) = t(1) >= t(2) >= ... >= x for any natural number x. Obviously t(0) is minimal among all terms having at least one t, which should make t(0) the ordinal w. The one disconcerting thing here is that initiality has made t(0) an infinite sup even though I assumed only finite sups. I don't know whether this means that the methods of J&M can't construct this initial algebra, or that in every topos with NNO one can construct the requisite sup-semilattices with countable sups. I suppose it must be the latter. (I'm a complete novice here, as I've said before, so I hope people will be patient with my appalling ignorance of topos-theoretic techniques.) Vaughan From rrosebru@mta.ca Sun Feb 22 02:23:31 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 22 Feb 2009 02:23:31 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lb7kN-00063L-0f for categories-list@mta.ca; Sun, 22 Feb 2009 02:23:27 -0400 From: Thomas Streicher Date: Sat, 21 Feb 2009 19:17:59 +0100 To: Paul Taylor , Subject: categories: Re Dedekind versus Cauchy reals MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Sender: categories@mta.ca Precedence: bulk Reply-To: Thomas Streicher Message-Id: Status: O X-Status: X-Keywords: X-UID: 68 Dear Paul and Andrej, I was aware of the fact that locatedness is part of definition of Dedekind cut it guarantees. It guarantees that there are close enough approximations for any required degree of precision. Having had a look at Andrej's slides I can't say that they provided me with an understanding of the operational semantics of the language. The impression I got is that he is using (kind of) interval arithmetic for determining truth values of terms of type \Sigma. That's ok but doesn't answer the question what is a computationally given real number. Do I understand your approach correctly as follows: when given a Dedekind cut as a mapping c : Q -> 2_\bot and an accuracy eps then \exists p,q : Q c(p) = 0 /\ c(q) = 1 /\ q-p < eps is true and computing this truth value gives the witnesses p and q. I.e. one evaluates terms of type \Sigma of the ASD language in a way reminiscent of logic programming. Thomas From rrosebru@mta.ca Mon Feb 23 01:33:32 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 23 Feb 2009 01:33:32 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LbTQY-00028p-EA for categories-list@mta.ca; Mon, 23 Feb 2009 01:32:26 -0400 Mime-Version: 1.0 (Apple Message framework v624) Content-Type: text/plain; charset=US-ASCII; format=flowed Content-Transfer-Encoding: 7bit From: Paul Taylor Subject: categories: Dedekind versus Cauchy reals Date: Sun, 22 Feb 2009 14:09:29 +0000 To: Categories list Sender: categories@mta.ca Precedence: bulk Reply-To: Paul Taylor Message-Id: Status: O X-Status: X-Keywords: X-UID: 69 Thomas Streicher asked about the "operational semantics" of the ASD calculus, and in particular computation with Dedekind cuts. As he says, the public documentation is rather limited at the moment, but Andrej and I don't want to give all our ideas away before we have made good use of them ourselves. The first thing that one should say about "operational semantics" is that mathematical formulae do NOT come with a prescibed way of computing them. A large part of what makes mathematics interesting is that there may be many ways of looking at a problem, besides the "obvious" one. The two situations in which notation does come with a preferred way of computing with it are long multiplication and lambda calculus, but even these cases are open to INGENUITY in finding better algorithms. > I was aware of the fact that locatedness is part of definition of > Dedekind cut it guarantees. It guarantees that there are close enough > approximations for any required degree of precision. Yes. In fact, there are two notions of locatedness, and this is the stronger one, which is necessary for arithemetic. There are some comments linking these ideas to the Archimedean axiom and the Conway numbers in Sections 11 and 12 of "The Dedekind reals in ASD". > when given a Dedekind cut as a mapping c : Q -> 2_\bot and an > accuracy eps then > > \exists p,q : Q c(p) = 0 /\ c(q) = 1 /\ q-p < eps > > is true and computing this truth value gives the witnesses p and q. Yes, that's right, except that "a mapping c : Q -> 2_\bot" is not a very helpful way of formulating it. When computing a real number, what we have (going back very clearly to Archimedes) is a pair of logical formulae, each with a single free variable (p and q in your notation, d and u in ours). One of which says when p is less than the real number being computed, and the other when q is greater. In order to fix the precision, we add another constraint that squeezes them close together. Then, as Thomas rightly says, > one evaluates terms of type \Sigma of the ASD language in a way > reminiscent of logic programming. He claimed that this > doesn't answer the question what is a computationally given real > number. Yes, it does, exactly. Notice that the "real number" is only on the "outside" of the computation, and is only manifested when we want to print it out --- hence my earlier pun that it is "peripheral". The "guts" of the computation are with LOGICAL formulae. > The impression I got is that he is using (kind of) interval > arithmetic for determining truth values Yes, but interval arithmetic is only one of a variety of tools. Also, if you only think of intervals as a way of computing real numbers to a given precision, you miss their real power. Plainly, these intervals just get wider and wider. Really, one should think of interval analysis as USING CRUDE ARITHMETIC TO DERIVE STRONG LOGICAL INFORMATION ABOUT FUNCTIONS. For example, if, when a function f is applied to an interval [d,u] using Moore arithmetics, the result f[d,u] lies within an interval (e,t), which we may determine purely ARITHMETICALLY, then we know the LOGICAL statement that All x:[d,u]. e < f(x) < t. Since f is given, not just as a funtion in the set-theoretic sense of a collection of input--output pairs, but as a FORMULA in a certain language, we may differentiate it formally, and apply interval arithmetic to that, obtaining even stronger LOGICAL information about the behaviour of the function. Examining the language, the real work consists of manipulating inequalities between polynomials over certain ranges of the variables. Often we just want to know whether the inequality ALWAYS, SOMETIMES or NEVER holds. A simple way to answer this question may just be Moore-wise evaluation, Then there is the sitation where the inequality is f(x,y) > 0 in a certain rectangle. The polynomial defines a curve (=0) and two regions (<0 and >0). As we increase the precision, the curve becomes closer to being a straight line, and the main numerical computation is of the gradient of this line, and of a narrow rectangle that encloses the curve. Just as the well known Moore arithmetic provides a way of evaluating universally quantified statments, so Kaucher arithmetic with back- to-front intervals answers existential statements. I don't want to go into more detail that this, because we want to get the credit for making this work (although we are keen to invove more collaborators). But also, these are just SOME of the things that might be done, AFTER ESCAPING FROM THE MENTAL STRAITJACKET of computation with Cauchy sequences or intervals. Paul Taylor From rrosebru@mta.ca Mon Feb 23 01:33:34 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 23 Feb 2009 01:33:34 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LbTRb-0002A3-9n for categories-list@mta.ca; Mon, 23 Feb 2009 01:33:31 -0400 Date: Sun, 22 Feb 2009 18:19:19 -0400 (AST) Subject: Re: categories: Fixing the constructive continued-fraction definition of the reals: proofs and refutations From: "Toby Kenney" To: "Vaughan Pratt" , categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: "Toby Kenney" Message-Id: Status: O X-Status: X-Keywords: X-UID: 70 The proof I gave is not quite ideal - I showed that if the objects 1-4 yo= u list all exist, then they are isomorphic. In theory, it would still be possible for object 3, say, not to exist. I think the following is a better proof: Let X be an object with morphisms 0 : 1 ----> X, s,t : X ----> X such tha= t ts=3Dt. We want to construct the map N^2 ----> X. We have a map f : N ----> X, given by considering X with just 0 and t. For every n in N= , we can also form a map g_n : N ----> X by g_n(0)=3Dt^n(0), and g_n(succ)=3D= s. Now we can form the map h : N^2 ----> X by h(a,b)=3Dg_a(b). I think this must be the unique map preserving everything necessary. Your suggestion of relaxing the condition to ts <=3D t seems to require changing from ordinary objects to partially-ordered objects. I think the initial one should be just the free monoid on two generators, with some partial order. You probably want to insist that s and t be inflationary. If you=B4re considering partially-ordered objects, then this won=B4t be isomorphic to N^2. I=B4m not sure whether there will be any isomorphism i= n the topos, even without requiring it to preserve order. You could alternatively consider a condition like t=3Dsts. I=B4m not really sure wh= at you mean by your claim that t is the ordinal w - I think the object you describe isn=B4t even totally ordered - how can you compare t^2(s(0)) and t^2(0)? If you take a condition like t=3Dsts to make it totally ordered, = you still have a decreasing chain t > ts > ts^2 > ... It looks like this should be something like the interval in N x Z, lexicographically ordered, going from (0,0) (so without the pairs (0,-n))= . If this is still an attempt to construct the reals, then I don=B4t see an= y sensible way to describe addition on an infinite lexicographic product of copies of Z (the integers). On the matter of it being disconcerting finding infinite sups, the definition doesn=B4t mention any form of partial order, so it shouldn=B4t really be any more surprising than finding (Kuratowski) finite sups. Sorry this email is mostly just intuition, rather than firm fact. Hopefully some wiser people than I will be able to put more substance to it. Toby > Toby Kenney wrote: >> Vaughan Pratt wrote in part: >>> I could well imagine 1 and 2 turning out to be isomorphic, but I feel= I >>> would get a lot from seeing the proof of whichever way that goes. > > Thanks very much, Toby. I didn't (and still don't) have any intuition > into what objects and morphisms are present in the free topos with NNO, > but your proof will help me fill in the gaps in this neighborhood of it= . > > On the one hand there are lots of objects one can talk about in languag= e > analogous to that characterizing the NNO, on the other there are also > lots of morphisms one can talk about that identify those objects (up to > isomorphism), and I'm still at the very early stage of learning how to > walk along that ridge line without falling off one side or the other. > > Joyal and Moerdijk, Algebraic Set Theory, show how to construct > sup-semilattices with sups up to a specified size S. Obviously not > every topos with NNO supports every S, but presumably S =3D K > (Kuratowski-finite) is always present. Your proof if correct shows tha= t > ts =3D t is too strong. What if I relax it to ts <=3D t and proceed as= in > J&M to construct the initial such object? Can you still construct your > isomorphism, or do we end up with a weaker relationship? If the latter > then we should have t(0) >=3D t(s(0)) =3D t(1) >=3D t(2) >=3D ... >=3D = x for any > natural number x. Obviously t(0) is minimal among all terms having at > least one t, which should make t(0) the ordinal w. > > The one disconcerting thing here is that initiality has made t(0) an > infinite sup even though I assumed only finite sups. I don't know > whether this means that the methods of J&M can't construct this initial > algebra, or that in every topos with NNO one can construct the requisit= e > sup-semilattices with countable sups. I suppose it must be the latter. > > (I'm a complete novice here, as I've said before, so I hope people will > be patient with my appalling ignorance of topos-theoretic techniques.) > > Vaughan > > From rrosebru@mta.ca Mon Feb 23 01:34:20 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 23 Feb 2009 01:34:20 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LbTSK-0002Ba-LQ for categories-list@mta.ca; Mon, 23 Feb 2009 01:34:16 -0400 Date: Sun, 22 Feb 2009 21:01:51 -0500 From: Jacques Carette MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Categorical development of algebra? Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: categories@mta.ca Precedence: bulk Reply-To: Jacques Carette Message-Id: Status: O X-Status: X-Keywords: X-UID: 71 Has anyone ever redone the classical development of algebra (magma, monoid, semigroup, quasigroup, group, ring, modules, etc) as appropriate diagrams in the Kleisli category of signatures and translations? Jacques From rrosebru@mta.ca Mon Feb 23 01:35:48 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 23 Feb 2009 01:35:48 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LbTTk-0002E8-Cx for categories-list@mta.ca; Mon, 23 Feb 2009 01:35:44 -0400 From: MFPS To: mfpsmail@tulane.edu, categories@mta.ca Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: MFPS Call for Participation Date: Sun, 22 Feb 2009 07:58:49 -0600 Sender: categories@mta.ca Precedence: bulk Reply-To: MFPS Message-Id: Status: RO X-Status: X-Keywords: X-UID: 72 Dear Colleagues, Registration is now open for MFPS 25, which will take place at Oxford from April 3 through April 7. A list of accepted papers and an outline program are also available. Participants will be housed either in University College or in Linton Lodge, a hotel located not far from the Computer Laboratory where the meetings will take place. We offer reduced registration fees for students and for faculty who attend only the last two days of the program. To register for the meeting, please point your browser at http://www.math.tulane.edu/~mfps/mfps25 Accommodations are being held only until March 24, so please register before then to reserve a room. Thanks, and best regards, Mike Mislove Mathematical Foundations of Programming Semantics http://www.math.tulane.edu/~mfps From rrosebru@mta.ca Mon Feb 23 19:22:11 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 23 Feb 2009 19:22:11 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lbk73-0002Cj-9s for categories-list@mta.ca; Mon, 23 Feb 2009 19:21:25 -0400 From: Michael Fourman To: Paul Taylor , Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v930.3) Subject: categories: Re: Dedekind versus Cauchy reals Date: Mon, 23 Feb 2009 09:03:51 +0000 Sender: categories@mta.ca Precedence: bulk Reply-To: Michael Fourman Message-Id: Status: O X-Status: X-Keywords: X-UID: 73 On 22 Feb 2009, at 14:09, Paul Taylor wrote: > don't want to give all our ideas away before we have > made good use of them ourselves Others who adopted this approach, long ago, have since become frustrated that they get no credit for ideas that (yet) others have independently (re)invented. Publish or perish! Professor Michael Fourman FBCS CITP Head of School Informatics Forum 10 Crichton Street Edinburgh EH8 9AB http://homepages.inf.ed.ac.uk/mfourman/ For diary appointments contact : ajudd(at)ed-dot-ac-dot-uk +44 131 650 2690 From rrosebru@mta.ca Mon Feb 23 19:22:11 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 23 Feb 2009 19:22:11 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lbk5N-00027N-5Y for categories-list@mta.ca; Mon, 23 Feb 2009 19:19:41 -0400 Date: Mon, 23 Feb 2009 00:16:37 -0800 From: Vaughan Pratt MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Fixing the constructive continued-fraction definition of the reals: proofs and refutations Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: quoted-printable Sender: categories@mta.ca Precedence: bulk Reply-To: Vaughan Pratt Message-Id: Status: O X-Status: X-Keywords: X-UID: 74 Toby Kenney wrote: > I think the following is a better proof: Toby, thanks for that. Peter J. suggested a proof in a separate email to me, let me absorb and compare them. > Your suggestion of relaxing the condition to ts <=3D t seems to require > changing from ordinary objects to partially-ordered objects. I think th= e > initial one should be just the free monoid on two generators, with some > partial order. You probably want to insist that s and t be inflationary= . Quite right, I forgot to specify that s and t were monotone (which implies inflationary), and I also left out that 0 is the empty sup.=20 (According to J&M in "Algebraic Set Theory" 1995, specifying=20 inflationary rather than monotone for the class as a whole gives the=20 hereditarily transitive sets, i.e. the von Neumann ordinals. Monotone=20 gives a larger class and a weaker notion of ordinal which nonetheless is=20 inflationary as a consequence of monotonicity and initiality.) > If you=B4re considering partially-ordered objects, then this won=B4t be > isomorphic to N^2. I=B4m not sure whether there will be any isomorphism= in > the topos, even without requiring it to preserve order. You could > alternatively consider a condition like t=3Dsts. I=B4m not really sure = what > you mean by your claim that t is the ordinal w - I think the object you > describe isn=B4t even totally ordered - how can you compare t^2(s(0)) a= nd > t^2(0)? If you take a condition like t=3Dsts to make it totally ordered= , you > still have a decreasing chain t > ts > ts^2 > ... The conditions I forgot to mention, 0 <=3D x and t monotone, should give=20 t^2(0) <=3D t^2(s(0)). > It looks like this should be something like the interval in N x Z, > lexicographically ordered, going from (0,0) (so without the pairs (0,-n= )). > If this is still an attempt to construct the reals, then I don=B4t see = any > sensible way to describe addition on an infinite lexicographic product = of > copies of Z (the integers). If both coordinates still have complemented subobjects, in particular if=20 {0} x w and w x {0} are both complemented subobjects, then I should=20 throw in the towel, consistent with Peter's advice. Are they? If w x=20 {0} is not a complemented subobject then we're moving in the right=20 direction: the next step is to define a suitable final coalgebra. Vaughan From rrosebru@mta.ca Thu Feb 26 02:51:21 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 26 Feb 2009 02:51:21 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lca2p-0003G3-DV for categories-list@mta.ca; Thu, 26 Feb 2009 02:48:31 -0400 Date: Wed, 25 Feb 2009 20:08:48 -0500 (EST) From: Michael Barr To: Categories list Subject: categories: ticked arrowheads in xy-pic and diagxy MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Michael Barr Message-Id: Status: O X-Status: X-Keywords: X-UID: 75 A month or two ago, Micah McCurdy wrote to ask me if it was possible to make an arrow with a tick in the middle (that is ----+---->) and I said I didn't know how to do that and suggested he ask Ross Moore. Ross told him that xy-pic didn't have that capacity. Well, Micah discovered that it did. Here are some samples, using diagxy, but that is just a front end to xy-pic. $$\bfig \node a(0,0)[A] \node b(300,400)[B] \arrow/@{>}|-*@{>}/[a`b;f] \efig$$ $$\bfig \ptriangle/>`>`@{>}|-@{|}/[A`B`C;f`g`h] \efig$$ $$\bfig \morphism/@{>}|-@{+}/<700,0>[ABCDE`F;h] \efig$$ $$\bfig \morphism/@{>}|-*@{|}/<700,0>[ABCDE`F;h] \efig$$ As far as I can tell, the * between the - and the @ has no effect. The one limitation is that what goes inside the -@{ } must be a \dir. This is a limitation for me, since I cannot figure out the syntax of \newdir. For this to work, it clearly has to be something that tex can rotate. Michael From rrosebru@mta.ca Thu Feb 26 02:51:21 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 26 Feb 2009 02:51:21 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lca1S-0003E1-Kg for categories-list@mta.ca; Thu, 26 Feb 2009 02:47:06 -0400 Date: Wed, 25 Feb 2009 20:52:02 +0600 (NOVT) From: "Serge P. Kovalyov" To: categories@mta.ca Subject: categories: Re: Question on E-coreflective subcategories MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: "Serge P. Kovalyov" Message-Id: Status: O X-Status: X-Keywords: X-UID: 76 Dear Colleagues, > Let A be a full isomorphism-closed coreflective subcategory of a > category C, G : C -> A be a coreflection. Let (E, M) be a factorization > system for C-morphisms, such that class G(E) contains class of all > A-isomorphisms and is contained in class of all A-retractions. > Is any of the following statements correct: > 1. If functor G preserves M, then it preserves E. > 2. If any M-morphism is mono, then an M-morphism belongs to Mor(A) > provided that its codomain belongs to Ob(A). John Kennison provided me with excellent counter-example to both statements. They are found in settings where M is "large" enough. Specifically, (1) is refuted as follows: Let C = Sets x {0,1} where {0,1} is the ordered category with 0 < 1. Then E = All isos of C plus all maps (f,1):(S,1) to (T,1) with f onto. And M = All maps (f,1):(S,1) to (T,1) with f one-to-one plus all maps from (S,0) And A = Sets x {0} (2) is refuted by taking an order with cardinality > 2, a minimum element, and a maximum element, for C, {min C, max C} for A, and (Iso, Mor) for factorization system on C. John suggested the simplest example, 3-chain 0 < 1 < 2. Thanks, Serge. From rrosebru@mta.ca Thu Feb 26 02:51:21 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 26 Feb 2009 02:51:21 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Lca2A-0003F7-5c for categories-list@mta.ca; Thu, 26 Feb 2009 02:47:50 -0400 Date: Wed, 25 Feb 2009 21:30:10 +0100 From: Carlos Areces Subject: categories: E. W. Beth Dissertation Prize: 2009 call for submissions Content-type: text/plain To: undisclosed-recipients:; Sender: categories@mta.ca Precedence: bulk Reply-To: Carlos Areces Message-Id: Status: O X-Status: X-Keywords: X-UID: 77 E. W. Beth Dissertation Prize: 2009 call for submissions Since 2002, FoLLI (the European Association for Logic, Language, and Information, www.folli.org) awards the E. W. Beth Dissertation Prize to outstanding dissertations in the fields of Logic, Language, and Information. We invite submissions for the best dissertation which resulted in a Ph.D. degree in the year 2008. The dissertations will be judged on technical depth and strength, originality, and impact made in at least two of the three fields of Logic, Language, and Computation. Inter-disciplinarity is an important feature of the theses competing for the E. W. Beth Dissertation Prize. Who qualifies. ~~~~~~~~~~~~~~ Nominations of candidates are admitted who were awarded a Ph.D. degree in the areas of Logic, Language, or Information between January 1st, 2008 and December 31st, 2008. There is no restriction on the nationality of the candidate or the university where the Ph.D. was granted. After a careful consideration, FoLLI has decided to accept only dissertations written in English. Dissertations produced in 2008 but not written in English or not translated will be allowed for submission, after translation, also with the call next year (for 2009). Respectively, nominations of full English translations of theses originally written in other language than English and defended in 2007 and 2008 will be accepted for consideration this year, too. Prize. ~~~~~~ The prize consists of: * a certificate * a donation of 2500 euros provided by the E. W. Beth Foundation. * an invitation to submit the thesis (or a revised version of it) to the new series of books in Logic, Language and Information to be published by Springer-Verlag as part of LNCS or LNCS/LNAI. (Further information on this series is available on the FoLLI site) How to submit. ~~~~~~~~~~~~~~ Only electronic submissions are accepted. The following documents are required: 1. the thesis in pdf or ps format (doc/rtf not accepted); 2. a ten page abstract of the dissertation in ascii or pdf format; 3. a letter of nomination from the thesis supervisor. Self-nominations are not admitted: each nomination must be sponsored by the thesis supervisor. The letter of nomination should concisely describe the scope and significance of the dissertation and state when the degree was officially awarded; 4. two additional letters of support, including at least one letter from a referee not affiliated with the academic institution that awarded the Ph.D. degree. All documents must be submitted electronically to bethaward2008@gmail.com. Hard copy submissions are not admitted. In case of any problems with the email submission or a lack of notification within three working days after submission, nominators should write to goranko@maths.wits.ac.za or policriti@dimi.uniud.it, with a cc to bethaward2008@gmail.com. Important dates: Deadline for Submissions: March 16, 2009. Notification of Decision: July 1, 2009. Committee : * Anne Abeill=C3=A9 (Universit=C3=A9 Paris 7) * Natasha Alechina (University of Nottingham) * Wojciech Buszkowski (Adam Mickiewicz University, Poznan) * Didier Caucal (IGM-CNRS) * Nissim Francez (The Technion, Haifa) * Valentin Goranko (chair) (University of the Witwatersrand, Johannesburg= ) * Alexander Koller (Saarland University) * Alessandro Lenci (University of Pisa) * Gerald Penn (University of Toronto) * Alberto Policriti (Universit=C3=A0 di Udine) * Rob van der Sandt (University of Nijmegen) * Colin Stirling (University of Edinburgh) From rrosebru@mta.ca Sun Mar 1 18:13:18 2009 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sun, 01 Mar 2009 18:13:18 -0400 Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LdtrI-0005tR-Of for categories-list@mta.ca; Sun, 01 Mar 2009 18:10:04 -0400 Date: Sat, 28 Feb 2009 11:55:34 -0500 (EST) From: Michael Barr To: Categories list Subject: categories: More arrow decorations MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed Sender: categories@mta.ca Precedence: bulk Reply-To: Michael Barr Message-Id: Status: O X-Status: X-Keywords: X-UID: 78 By playing with Micah's discovery (which is actually documented on page 39, third line from the bottom of Fig. 13), I have come up with the following potentially useful decorations: $$\bfig \morphism/@{>}|-@{|}/<500,500>[A`B;f] \efig$$ $$\bfig \morphism/@{>}|-@{x}/<500,500>[A`B;f] \efig$$ $$\bfig \morphism/@{>}|-@{o}/<500,500>[A`B;f] \efig$$ $$\bfig \morphism/@{>}|-@{*}/<500,500>[A`B;f] \efig$$ $$\bfig \morphism/@{>}|-@{||}/<500,500>[A`B;f] \efig$$ $$\bfig \morphism/@{>}|-@{)}/<500,500>[A`B;f] \efig$$ $$\bfig \morphism/@{>}|-@{(}/<500,500>[A`B;f] \efig$$ The same ideas also work in native xy-pic and, for all I know, in the matrix version as well. Michael