Date: Mon Jan 26 21:40:18 1998 Subject: Friedman's challenge The reason why 1970s topos theorists did a "slavish translation" of well-pointedness, choice, etc is quite simple: it is known in computer science and engineering as "reverse compatibility". We (ie Lawvere, Tierney and others) needed to show that whatever you could allegedly do with set theory, you could do with elementary toposes too. Now that reverse compatibility has been achieved, the old methods are obsolete, and we should be able to move on from there. We show that the new methods (by which I mean category theory in general, not necessarily elementary toposes) are more idiomatic for the old purposes and more powerful for new ones. For example we would never have got anywhere with domain models of polymorphism, or with synthetic domain theory, without category theory as our guide. I'm sure that most of the readers of "categories" can add examples from their own interests. I have a personal reason for bitterly resenting ever being taught set theory. (I don't want anybody to interpret that as resentment towards the particular people in Cambridge who did the teaching - the problem is with the mathematical community as a whole which has perpetuated this pernicious theory.) For several years I was trying to prove (in an elementary topos, in particular without excluded middle, or the axiom of collection, which seems to me to be set-theoretic hocus pocus): Let (X, <=) be a poset with least element and directed joins, and s:X->X a monotone (not necessarily Scott continuous) function. Then s has a least fixed point. I talked about my attempts at this at at least two international category meetings and several other project meetings and conferences. Because of my set-theoretic indoctrination, much as I rebelled against it, I set about defining ordinal iterates of the function s and its values at the least element. The intuitionistic theory of ordinals is complicated, and there are several flavours of them, but there is no doubt that ordinals as big as you please exist in any elementary topos. See JSL 61 (1996) 703-742. Always with traditional applications of ordinals, the problem is knowning when to stop. The textbook solution is due to Friedrich Hartogs, 1917. Basically, you take a pair of scissors ... . Andre Joyal and Ieke Moerdijk have a pair of scissors which make a cleaner cut (by our standards in category theory), but they too still chop off the standard sequence. (Maybe someone would like to write a PhD thesis which uses their methods to eliminate the set theory from the "alpha-presentable" versions of Gabriel-Ulmer duality.) In fact this result has now been proved, by a Georgian called Dimitri Pataraia. (I haven't met him, or been able to find out much about him, despite now sharing an office with another Georgian). Pataraia's solution is pure order theory. You could teach it to a third year undergraduate class in a course on lattices or domain theory. There is not an ordinal in sight. In fact, looking more closely at his solution, there *are* ordinals in it. [My version of] his proof looks remarkably like Zermelo's second proof of Choice => well ordering. It may seem strange that such an infamously classical result should contain a the essence of an intuitionistic argument, but in fact [Zermelo's version of] Choice occurs in the first line of the argument and never again. Zermelo manufactures the required ordinal structure out of the given object, whereas the subsequent orthodox approach, due to Hartogs 9 years later, is based on a single monolithic system, which has to be chopped off in a rather unceremonious fashion. Ordinals similar to Zermelo's, though only satisfying the induction scheme for a restricted class of predicates, and not satisfying any recursion scheme I can find, are also to be found in Pataraia's proof. Throughout my (personally unsuccessful) study of this problem, whenever I sought intuition from set theory it took me in the WRONG direction. I cannot think of any other branch of mathematics, with the exception of infinitessimal calculus before it was reformed, which I would condemn so utterly. In fact, 18th century calculus did give a lot of right answers, and at least its wrong ones were interesting and provoked good research. In answer to Harvey Friedman, I *don't* advocate topos theory as foundations. It still reeks of set theory (sorry, Bill). Paul Taylor =================================== Part II (it seems that I originally sent the above to the wrong email alias) I didn't properly spell out my philosophical conclusions about ordinals. What I mean is that a [not "the"] system of ordinals *ought* to have a top element (a fixed point for successor). In other words, I am contradicting the usual interpretation of the Burali-Forti paradox, and discarding the tradition of chopping the monolithic system of ordinals off, as Hartogs, Joyal/Moerdijk and many others have done (including me). The notion of cardinality is clearly stupid from a categorical point of view (we know better than to classify objects up to isomorphism, without even any regard to their automorphism groups) and, as an atheist, I find Cantor's theologically motivated notion of "size" utterly incomprehensible. While I'm at it, I don't accept the argument in either Russell's paradox (re the set {x:x not in x}) or Cantor's theorem that P(X) =/= X. It's not that I am particularly keen to have a set of all sets (though such a thing is probably to be expected from the right logical principles in much the same way as a universal Turing machine is in recursion theory), but that I do not consider that these classic arguments ought to be valid. Andy Pitts and I traced Russell's paradox to a particular quantifier (in fact in a locally cartesian closed category) - see our paper in Studia Logica 1989 p 387. It is this quantifier which I reject. In fact he and I independently had models which had a type of types, and achieved this by restricting the quantifiers which could be interpreted. The Burali-Forti paradox goes away too if the class of predicates for which the induction scheme is valid (in the definition of an ordinal) is retricted. For example, the domain of increasing natural numbers plus a fixed point is such an ordinal for Scott-continuous predicates (the Crole-Pitts FIX object). I think I may be able to adjust the notion of elementary topos (I prefer to think in these terms than in symbolic logic) to a useful fragment in which Cantor's theorem fails. (Sorry to be so vague, but I haven't got very far with this, and currently have a head full of perl programming.) Paul