From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/620 Path: news.gmane.org!not-for-mail From: categories Newsgroups: gmane.science.mathematics.categories Subject: Re: Challenge from Harvey Friedman Date: Wed, 28 Jan 1998 10:09:34 -0400 (AST) Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241017076 26547 80.91.229.2 (29 Apr 2009 14:57:56 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 14:57:56 +0000 (UTC) To: categories Original-X-From: cat-dist Wed Jan 28 10:10:05 1998 Original-Received: (from cat-dist@localhost) by mailserv.mta.ca (8.8.8/8.8.8) id KAA01244; Wed, 28 Jan 1998 10:09:34 -0400 (AST) Original-Lines: 60 Xref: news.gmane.org gmane.science.mathematics.categories:620 Archived-At: 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.