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