[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
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
On Friday 30 January 2009 08:18:39 Galchin, Vasili wrote:
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?
Yes, it exists. In fact, it is a continuous image of 2^N. It is Bishop compact, fan-like and compact overt (choose your taste of constructivism). Bas
I don't think it exists from a constructivist viewpoint because it has to be constructed in a finite number of steps. Vasili On Fri, Jan 30, 2009 at 3:52 PM, Bas Spitters <spitters@cs.ru.nl> wrote:
On Friday 30 January 2009 08:18:39 Galchin, Vasili wrote:
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?
Yes, it exists. In fact, it is a continuous image of 2^N. It is Bishop compact, fan-like and compact overt (choose your taste of constructivism).
Bas
i.e. a well-defined algorithm exists to construct Cantor dust but the Cantor dust cannot be constructed/built from the algorithm in a finite number of steps. Hence, Cantor dust represents potential infinity rather than actual infinity. This problem has nagged at me for a while. Regards, Vasili On Fri, Jan 30, 2009 at 4:40 PM, Galchin, Vasili <vigalchin@gmail.com>wrote:
I don't think it exists from a constructivist viewpoint because it has to be constructed in a finite number of steps.
Vasili
On Fri, Jan 30, 2009 at 3:52 PM, Bas Spitters <spitters@cs.ru.nl> wrote:
On Friday 30 January 2009 08:18:39 Galchin, Vasili wrote:
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?
Yes, it exists. In fact, it is a continuous image of 2^N. It is Bishop compact, fan-like and compact overt (choose your taste of constructivism).
Bas
It seems that what you are describing is usually called finitism. Bas On Saturday 31 January 2009 05:35:41 Galchin, Vasili wrote:
i.e. a well-defined algorithm exists to construct Cantor dust but the Cantor dust cannot be constructed/built from the algorithm in a finite number of steps. Hence, Cantor dust represents potential infinity rather than actual infinity. This problem has nagged at me for a while.
Regards, Vasili
Galchin, Vasili wrote:
i.e. a well-defined algorithm exists to construct Cantor dust but the Cantor dust cannot be constructed/built from the algorithm in a finite number of steps. Hence, Cantor dust represents potential infinity rather than actual infinity. This problem has nagged at me for a while.
Bill, if you mean this literally then you don't accept the existence of the set N of natural numbers either. If that's the case then for you it is very reasonable to reject the Cantor set K as well, e.g. because you're a finitist as Bas Spitters suggests. However if you're ok with the idea of a natural numbers object N in a topos, defined as an initial algebra for the functor F(X) = X+1, then you would need to draw a fairly fine line to reject as nonconstructive a Cantor set object K in a topos, defined as a final coalgebra for the functor F(X) = 2X (~ X+X, 2 being 1+1 in a topos). From this standpoint the existence of a Cantor set object is more plausible than a continuum object rather than less because more is needed. If you go with the double-induction approach of Pavlovic and Pratt, where the functor is F(X) = NX (~ X+X+X+...) then the topos needs a natural numbers object. If instead you go with Freyd's single-induction approach of connecting up (eliminating the gap between) the two halves of K+K, as preferred e.g. by Tom Leinster, then the topos needs structure sufficient tfor such gluing. 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? Vaughan Pratt
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
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
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
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
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
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
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
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
Quoting "Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>:
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.
Even if one insists that constructive entails predicative the appropriateness of Cauchy reals is questionable: Lubarsky and Rathjen prove in fact that in a 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 generally 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 intuitionistic 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
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
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
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 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
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
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
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
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
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
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.
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". <snip>
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"). <snip>
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.
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.
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
QUESTION 2: is there a branch of constructivism that would reject as 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
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
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
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
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
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
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
On Tue, Feb 10, 2009 at 4:18 PM, Prof. Peter Johnstone <P.T.Johnstone@dpmms.cam.ac.uk> 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
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
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
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 <http://www.springerlink.com/index/f5547884k02u112q.pdf>[1]. Then, using the type schemes devised by Luis Caires<http://ctp.di.fct.unl.pt/~lcaires/papers/CALCO-Caires-1.0.pdf> , 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 <http://www.csc.kth.se/~mfd/Papers/pspcl.pdf> 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
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
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
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
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
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
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
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
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
participants (15)
-
Bas Spitters -
Bhupinder Singh Anand -
Dusko Pavlovic -
Galchin, Vasili -
gcuri＠math.unipd.it -
Greg Meredith -
Michael Shulman -
Paul Taylor -
Prof. Peter Johnstone -
spitters
-
Steve Stevenson -
Toby Bartels -
Toby Bartels -
Toby Kenney -
Vaughan Pratt