Re: Friedman's challenge, and the ordinals

Re: Friedman's challenge, and the ordinals

[categories]

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

Friedman's challenge, and the ordinals

[categories]

Date: Fri, 30 Jan 1998 19:11:18 GMT
From: Paul Taylor <pt@dcs.qmw.ac.uk>

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