Friedman's challenge, and the ordinals

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

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