Re: Challenge from Harvey Friedman

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

Date: Tue, 27 Jan 1998 11:26:45 +0000 (GMT)
From: Dusko Pavlovic <D.Pavlovic@doc.ic.ac.uk>

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.