Re: Friedman's challenge, and the ordinals

[categories <cat-dist@mta.ca>]

Date: Sat, 31 Jan 1998 16:21:53 +0000 (GMT)
From: Dr. P.T. Johnstone <P.T.Johnstone@dpmms.cam.ac.uk>

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