Date: Fri, 23 Jan 1998 16:27:33 -0400 (AST)
Subject: Challenge from Harvey Friedman
Date: Fri, 23 Jan 1998 11:11:28 -0800
From: Vaughan Pratt
I'm taking the liberty of forwarding to the categories mailing list
the following challenge posted by Harvey Friedman to Steve Simpson's
Foundations of Mathematics mailing list.
This is the latest in a long-running engagement about sets vs.
categories on the latter list, recent postings to which can be read at
http://www.math.psu.edu/simpson/fom/postings/9801.html
Postings with "categor{y,ical}" in their subject lines are the relevant
ones.
Information about the fom list (how to subscribe etc.) can be found at
http://www.math.psu.edu/simpson/fom/fom-info
As we were fond of saying quarter of a century ago,
Peace
Vaughan Pratt
------- Forwarded Message
Date: Fri, 23 Jan 1998 00:54:20 +0100
To: fom@math.psu.edu
From: Harvey Friedman
Subject: FOM: Set Theory Axioms
The point of this posting is to give some entirely conventional axioms for
set theory that are a bit simpler than many that are normally given. They
are fully formal. By comparison, look at the axioms of elementary topoi
that are given in MacLane/Moerdijk, Sheaves in Geometry and Logic, A first
Introduction to Topos Theory, Springer-Verlag, 1994, on p. 163. The
difference in complexity is strikingly grotesque.
I challenge anyone to write down their favorite fully formal axioms for
topoi that are sufficient to do real analysis, so we can compare them side
by side with the fully formal axioms I write down here.
Topos theory with natural number object is insufficient to develop
undergraduate real analysis - although many fom postings conceal this fact.
One has to add to topoi: natural number object, well pointedness, and
choice. The latter two are nothing more than slavish translations of set
theory into the topos framework. The "idea" is to take a fatally flawed
foundational idea and force it to "work" by transporting important ideas
from set theoretic foundations.
But the axioms of elementary topoi are already incomparably more
complicated than the axioms for set theory presented here.
Let me start with the dramatically simple axioms of finite set theory.
These amazingly simple axioms are tremendously powerful. We work in the
usual classical predicate calculus with equality and one binary relation
symbol epsilon - which we abbreviate here by "in." It is also useful to use
the constant symbol 0 (for the empty set), the unary function symbol { }
(for singletons), and the binary function symbol U (for pairwise union).
Note that axioms 2-4 amount to the most trivial of definitions.
1. (forall x)(x in a iff x in b) implies a = b.
2. (forall x)(not(x in 0)).
3. x in {a} iff x = a.
4. x in a U b if and only if (x in a or x in b).
5. [phi(0) & (forall x,y)((phi(x) & phi(y)) implies phi(x U {y}))] implies
phi(x).
Here phi(x) is any formula in the language in which y is not free.
That's all! One ***derives*** pairing, union, power set, foundation,
replacement, and choice, from these axioms alone!!! Also, when
appropriately formalized, "every set is finite" and things like "every set
has a transitive closure." These axioms are "practically" complete - an
informal concept that I have alluded to before on the fom.
Now for ZFC. We take a different tack and only use epsilon.
1. (forall x)(x in a iff x in b) implies a = b.
2. (therexists x)(a in x & b in x).
3. (therexists x)(forall y in a)(forall z in y)(z in x).
4. (therexists x)(forall y)((forall z in a)(z in y) implies y in x).
5. (forall x,y)(x in y implies (therexists z in y)(forall w in z)(w notin y)).
6. (therexists x,y)(x in y & (forall z in y)(therexists w in y)(z in w)).
7. (therexists x)(forall y)(y in x iff (y in a & phi)), where phi is any
formula in the language in which x is not free.
8. (forall x in a)(therexists y)(phi) & (forall x,y,z)((phi(x,z) &
phi(y,z)) implies x = y) implies (therexists w)(forall x in a)(therexists
unique y in w)(phi),
A novelty is the axiom of infinity, 6, is simpler than usual; and also
choice and replacement are combined nicely by 8. This allows such a simple
axiomatization in purely primitive notation. Try to right down the axioms
of a topos with natural number object, well pointed, and choice, in simple
primitive notation!! Good luck.
As is well known, ZFC is "practically" complete.
The version in the book on p.163 - which does not even include natural
number object, well pointedness, or choice - requires a very substantial
amount of preliminary abbreviations in order to formalize.
------- End of Forwarded Message
Date: Fri, 23 Jan 1998 19:38:46 -0400 (AST)
Subject: Re: Challenge from Harvey Friedman
Date: Fri, 23 Jan 1998 16:32:35 -0600 (CST)
From: David Yetter
Dear Fellow Categorists:
I am personally not likely to take up Harvey Friedman's challenge,
having long been doing "category theory as algebra" rather than "category
theory as foundations".
I would like to point out, though that Friedman has deliberately chosen
as a test case real analysis, a subject which exists only to simulate the
existence of fluxions on the basis of foundations tied to two-valued logic.
How about asking Friedman to give an elegant, elementary foundation for
rings satisfying the Kock-Lawvere axioms?
The use of an axiom schema in which arbitrarily complex formulae
may be subsituted also seems a bit of a dodge. At first glance, elementary
topoi plus NNO, well-pointed and choice still doesn't need such things
(but I could be wrong, not having thought much about it for years).
Best Thoughts,
David Yetter
Date: Sat, 24 Jan 1998 13:34:28 -0400 (AST)
Subject: Re: Challenge from Harvey Friedman
Date: Fri, 23 Jan 1998 21:22:39 -0500 (EST)
From: Michael Barr
I guess simplicity is in the eye of the beholder. For example, I do not
consider the categorical version of either choice (epis split) or
well-pointed (1 is a generator) to be translations of set theory, but
perfectly natural categorical axioms. The point is that Harvey is a
set-theorist, so he thinks comprehension and all that stuff (which at
least 95% of all mathematicians could not state properly if their lives
depended on it) is perfectly natural and I don't.
But my actual criticism of ZF(C) is much simpler. I have taught these
courses in set theory and we spend a lot of time developing these epsilon
trees and then totally ignore the structure. In other words, the epsilon
tree structure of sets is totally irrelevant to what you do with them.
There are a number of definitions of pairs, but they are irrelevant. The
only thing we need to know about pairs (and the only thing a categoriest
does know) is when two pairs are equal. All the defintions of pairs have
that property of course, but they also have irrelevant properties.
Mike
Date: Sat, 24 Jan 1998 13:35:31 -0400 (AST)
Subject: Re: Challenge from Harvey Friedman
Date: Sat, 24 Jan 1998 15:59:46 +0000 (GMT)
From: Dr. P.T. Johnstone
> But the axioms of elementary topoi are already incomparably more
> complicated than the axioms for set theory presented here.
What on earth does Friedman mean by complicated? As Peter Freyd
pointed out a long time ago, the axioms for an elementary topos are
essentially algebraic -- that is, they live at a very low level
of logical complexity. The very first axiom in anyone's (including
Friedman's) axiomatization of set theory is the axiom of
extensionality, which is not expressible even in coherent logic
(at least, not unless you take not-membership as a primitive
predicate, on the same level as membership).
Unless Friedman can put forward an objective measure of complexity
(as opposed to "unfamiliarity to H. Friedman") which justifies the
above quote, then his challenge is not worth considering.
Peter Johnstone
Date: Mon, 26 Jan 1998 15:01:46 -0400 (AST)
Subject: Re: Challenge from Harvey Friedman
Date: Mon, 26 Jan 1998 14:21:40 +0000 (GMT)
From: Ronnie Brown
How does Harvey Friedman know that the formulation of real analysis as
carried out in set theory will do all that real analysis *should* do?
My favourite example is that of partial functions. Most teachers of real
analysis (calculus) rightly impress on students the importance of the domain
of a function,
and the domain of f+g, etc. So a student might think that the algebra and
analysis of partial functions would occupy a good part of the literature.
Solutions of ODEs (such as dy/dx=exp(-y) ) are often given by partial
functions
with domain involving a parameter, and the solution (including its
domain) seems to vary smoothly with this parameter. In fact there is very
little in the literature on such matters. I had a small go with
29. (with A.M. ABD-ALLAH), ``A compact-open topology on partial maps with
open domain'', {\em J. London Math Soc.} (2) 21 (1980) 480-486.
It is not clear that the most general case of
the functional analysis of partial functions with domain neither open nor
closed can be successfully handled within classical set theory. There is
a chance it can be handled within topos theory. (Try functions defined on
the leaves of foliations. Any answers?)
Another point of topos theory is to handle categories such as that of
directed graphs in a similar manner to the category of sets, and to make
comparisons between such categories. (Bill Lawvere has of course written
a lot on this.)
Ronnie Brown
Date: Mon, 26 Jan 1998 15:00:55 -0400 (AST)
Subject: Re: Challenge from Harvey Friedman
Date: Mon, 26 Jan 1998 12:10:01 +0000
From: Steven Vickers
>Topos theory with natural number object is insufficient to develop
>undergraduate real analysis - although many fom postings conceal this fact.
>One has to add to topoi: natural number object, well pointedness, and
>choice. The latter two are nothing more than slavish translations of set
>theory into the topos framework. The "idea" is to take a fatally flawed
>foundational idea and force it to "work" by transporting important ideas
>from set theoretic foundations.
The slavish translation of well pointedness and choice actually arises from
a more subtle slavish translation of point-set topology.
Point-set topology postulates that the points of a topological space can be
comprehended as a set, but this apparently innocuous idea is questionable
(perhaps we should be more sceptical about what sets can comprehend
following our experience with proper classes).
When we formulate our foundations based on the ideas of topos theory, and
interpret "set" as object in an elementary topos, then - given a natural
numbers object - we can ideed construct "sets of reals" but we find that
they misbehave. Normal theorems of analysis, such as Heine-Borel, fail
unless we also impose the additional ideas from set-theoretic foundations.
However, there is a different way of formulating topology, using locales or
"formal spaces", that works in any elementary topos (still need an NNO to
get the reals, of course) and preserves the validity of theorems such as
Heine-Borel. It works by addressing the topology directly, without regard
to what the opens in it might be sets of. It still has a concept of point,
but generalized point with respect to a varying set-theory (stage of
definition) instead in a fixed one. We can't take a single comprehension in
our favourite set-theory as encompassing all the points.
The moral is that a topological space is more than just a set of points
together with a topology of open subsets. If, for any reasons at all, we
are interested in doing mathematics constructively, then we should discard
point-set topology and use locales.
My picture of what is going on is this: when we try to make a set out of a
space by stripping off the topology, we damage the points, and we put the
well-pointedness and choice in as crutches and plasters to try to rectify
the damage we should never have done in the first place.
Steve Vickers.
Date: Mon, 26 Jan 1998 14:59:09 -0400 (AST)
Subject: Re: Challenge from Harvey Friedman
Date: Sun, 25 Jan 1998 10:13 +0530
From: CAYLEY@tifrvax.tifr.res.in
I remember to have seen a paper on frameworks for
measuring complexity of mathematical concepts by
two autors earlier. (I don't exactly recall where)
but I also remeber that one of the authors was
H.Friedman!
P.S.Subramanian
Tata Institute.
Date: Mon, 26 Jan 1998 15:00:00 -0400 (AST)
Subject: Immodest proposal
Date: Sun, 25 Jan 1998 10:48:12 -0500 (EST)
From: John R Isbell
Contemplating Harvey Friedman's Challenge, I asked
myself 'Aren't there more important problems around?'
And of course there are. Moreover, I believe I have
solved one of them.
P. What should we call the ancient substitute for
e-mail?
S. Why not m-mail? Snappy; memorable; unmistakable;
and m=e\over {c^2} gives the value.
John Isbell
Date: Mon, 26 Jan 1998 19:34:55 -0400 (AST)
Subject: Re: Challenge from Harvey Friedman
Date: Mon, 26 Jan 1998 17:36:31 -0500 (EST)
From: John R Isbell
P. S. Subramanian's 'A framework for measuring ...
complexity' is by H. Friedman and R. C. Flagg, Adv.
in Appl. Math. 11 (1990), 1-34 [MR91f:03111].
John Isbell
Date: Wed, 28 Jan 1998 10:10:21 -0400 (AST)
Subject: Re: Challenge from Harvey Friedman
Date: Tue, 27 Jan 1998 11:26:45 +0000 (GMT)
From: Dusko Pavlovic
According to Harvey Friedman:
> I challenge anyone to write down their favorite fully formal axioms for
> topoi that are sufficient to do real analysis, so we can compare them side
> by side with the fully formal axioms I write down here.
The papers I announced here the other day do not offer any such
"dramatically simple" or "tremendously powerful" axioms, comparable
with Friedman's, nor indeed anything as politically engaged --- but I
think they may have to do with the issue.
Given a field in any category with enough limits, we implement
analytic functions, solve differential equations --- do quite a bit of
real analysis. It turns out that most of it can be captured as guarded
induction on final coalgebras.
We did not try to use this to embed real analysis in any fully formal
foundational theory, but to provide a uniform way of implementing it
on a computer, together with infinitary constructions and all. The
result may not be as "amazingly simple" as Friedman's axioms, but it
is fairly simple, and conceptually clear. Check it out (the last two
papers at http://www.cogs.susx.ac.uk/users/duskop/).
Sorry for the plug, but I actually want to make a point. I don't think
category theory should spend time trying to beat set theory on its own
territory of fully formal systems. Sets were invented in the time of
doubt about the consistency of mathematics, when foundations were
really sought for. Nowadays people go and prove Fermat Theorem.
Set theory wants to be something like a formal grammar of
mathematics. That is fine, can be very interesting in itself, but
great stories are usually told without thinking of grammar.
Category theory might perhaps do better to try to be some kind of a
programming language or mathematics, a set of object-(or better:
method-)oriented tools, conceptualizing large "software" projects of
the day.
How about that?
-- Dusko Pavlovic
PS On the other hand, us toposophers competing against them
setologists who can do analysis --- aren't we a bit like
A Frenchman and an Englishman making the bet who can faster
translate a sentence from German. Little Gretschen comes
by and says: (fg)' = f'g + fg'...
I mean, didn't analysts tell *everyone* by now: THEY DO NOT CARE FOR
FOUNDATIONS. They do not think of their manifolds neither as sets of
little elements, nor hanging on a bunch of morphisms among other
manifolds. Most of the time, they are quite happy with their manifolds
as manifolds. Next time they need foundations, they'll invent them
again, like they invented sets and sheaves.
Date: Wed, 28 Jan 1998 10:09:26 -0400 (AST)
Subject: The Friedman/Flagg paper
Date: Mon, 26 Jan 1998 19:16:12 -0500 (EST)
From: Peter Freyd
91f:03111 03E99 03B30 03F99 68Q25
Friedman, H.(1-OHS); Flagg, R. C.(1-SME)
A framework for measuring the complexity of mathematical concepts.
(English)
Adv. in Appl. Math. 11 (1990), no. 1, 1--34.
_________________________________________________________________
This paper presents a system $\scr F\sb 0(\scr B)$ that is intended to
allow practical computation of the complexity of mathematical
concepts. $\scr F\sb 0(\scr B)$ is an untyped theory of sets and
partial functions in a first-order free logic with equality and a
description operator. Its language $\scr L\sb 0(\scr B)$ contains many
primitive operations, such as $n$-tuples, lambda abstraction,
comprehension terms, finite set and Cartesian product formation, and
definition by cases. $\scr B$ denotes a set of "descriptive forms"
that are patterns according to which new constants, functions, and
predicates can be defined. After a rigorous presentation of the syntax
of $\scr L\sb 0(\scr B)$, standard programming language procedures
yield parsing and recognition algorithms. A precise semantics for
$\scr L\sb 0(\scr B)$ is given, followed by a deductive system $\scr
F\sb 0(\scr B)$ that is shown to be complete by means of a
Henkin-style proof. Finally, the authors introduce the notions of
definition sequence, definition dag (directed acyclic graph), and
definition tree. On the basis of these notions, they promise that, in
a future paper, they will develop measures of complexity of
definitions that will make possible practical calculation of the
complexity of concepts in a large part of current mathematical
practice.
Reviewed by E. Mendelson
Date: Thu, 29 Jan 1998 16:15:31 -0400 (AST)
Subject: Re: Challenge from Harvey Friedman
Date: Wed, 28 Jan 1998 22:15:27 +0000
From: Carlos Simpson
Being a newcomer to the category list, I have a really naive and stupid question
(concerning H. Friedman's challenge). Namely, I was always under the impression
that you had to know what a set was before you could talk about what a
category was (in particular a topos). Is it possible to talk about toposes
without knowing what a set is?
This seems somewhat related to a question that has been bugging me for some
time, namely how to talk about a ``category''
which is enhanced over itself, but not necessarily having any functor to or
from Sets. The very first part of the structure would be a class of objects
O
together with a function (x,y)\mapsto H(x,y) from O\times O to O, but I
can't get beyond that.
---Carlos Simpson
Date: Fri, 30 Jan 1998 15:56:00 -0400 (AST)
Subject: Re: Challenge from Harvey Friedman
Date: Fri, 30 Jan 1998 10:40:55 -0500 (EST)
From: Michael Barr
Well the first question has an easy answer. It is just as possible to
talk about a category without knowing what a set is as it is to talk about
a set without knowing what a set is. Of course, you cannot talk about
homsets. It is interesting to read the very first Eilenberg-Mac Lane
paper, which did not talk about homsets. A set is an undefined notion and
there is a relation, epsilon that may hold between one set and another,
subject to certain axioms, one version of which Friedman listed. A
category consists of undefined things called arrows and three relations,
two functional and the third partially functional (actually better than
that, but leave that aside). Friedman's axioms are not coherent, as has
been pointed out, while the categorical axioms are. On the other hand,
one can state Friedman's axioms, in all their glorious incomprehensibility
(I think I could stare at the 8th one from now until the middle of next
year without understanding what it says, and the 6th, asserted to be the
axiom of infinity is not much clearer) in a couple hundred words, while it
is pretty much necessary to interrupt the topos axioms for some
definitions (at least monic and subobject) to do the topos axioms. Thus
each one looks simpler to its devotees and there is really no point in
arguing about it.
Michael
On Thu, 29 Jan 1998, categories wrote:
> Date: Wed, 28 Jan 1998 22:15:27 +0000
> From: Carlos Simpson
>
> Being a newcomer to the category list, I have a really naive and stupid question
> (concerning H. Friedman's challenge). Namely, I was always under the impression
> that you had to know what a set was before you could talk about what a
> category was (in particular a topos). Is it possible to talk about toposes
> without knowing what a set is?
>
> This seems somewhat related to a question that has been bugging me for some
> time, namely how to talk about a ``category''
> which is enhanced over itself, but not necessarily having any functor to or
> from Sets. The very first part of the structure would be a class of objects
> O
> together with a function (x,y)\mapsto H(x,y) from O\times O to O, but I
> can't get beyond that.
>
> ---Carlos Simpson
>
>
>
Date: Fri, 30 Jan 1998 15:57:30 -0400 (AST)
Subject: Friedman's challenge, and the ordinals
Date: Fri, 30 Jan 1998 19:11:18 GMT
From: Paul Taylor
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
Date: Mon, 2 Feb 1998 10:10:45 -0400 (AST)
Subject: Re: Friedman's challenge, and the ordinals
Date: Sat, 31 Jan 1998 16:21:53 +0000 (GMT)
From: Dr. P.T. Johnstone
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