Some comments on Paul Taylor's diatribe:
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 -
Thanks, Paul!
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.
Well, perhaps you should have been blaming me after all. I clearly never got around to teaching you Ernst Witt's amazing proof (Beweisstudien zum Satz von M. Zorn, Math. Nachr. 4 (1951), 434--438) of the existence of fixed points for an s:X->X which is merely assumed to be inflationary (i.e. x \leq s(x) for all x \in X), and not necessarily monotone. (Of course, you can recover the result for monotone s by restricting to the subset \{x\in X | x \leq s(x)\}.) [I may say that I didn't discover this paper for myself; it was brought to my notice by Bernhard Banaschewski (who had obvious reasons for knowing about it). It appears that Brian Davey and Hilary Priestley also knew about it, since they included it as Theorem 4.14 in their "Introduction to Lattices and Order" (C.U.P., 1990), though they don't attribute it to Witt (or to anyone else).] Witt's proof, like Pataraia's, is entirely order-theoretic and uses only naive set theory; it is clearly inspired by Zermelo's second proof of the well-ordering theorem, to which Paul referred. What it does use, however, is the Law of Excluded Middle, in a way which seems absolutely inextricable from the proof. Nevertheless, I suspect that an extremely clever person, trying to constructivize Witt's proof, could have discovered the idea of Pataraia's. (I didn't, although I spent some ten years thinking about the problem on and off; Pataraia didn't either -- he told me in November that he wasn't aware of Witt's proof.)
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.
Indeed you could. The same is true of Witt's proof: I did teach it, last term, in my third-year logic course here in Cambridge. (The students found it quite tough going, but they managed to swallow it -- I think.) A couple of weeks later I learned of Pataraia's proof at the Aarhus PSSL meeting; so the students got that too, immediately after I returned to Cambridge. (They must think I'm obsessed with this particular theorem; perhaps they're right.) There remains an open problem, however. Pataraia's proof is constructive (that is, it works in any topos -- though it is impredicative, so the Martin-L\"of people won't accept it), but it does require the function s to be monotone as well as inflationary. So: can anyone find a constructive proof of Witt's original result (without the monotonicity assuption)? Peter Johnstone