From lusk Tue Jun 7 12:50:48 1994
Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id MAA03478 for ; Tue, 7 Jun 1994 12:48:48 0500
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk
with SMTP (PP6.5) to cl; Tue, 7 Jun 1994 18:48:30 +0100
To: qed@mcs.anl.gov
Subject: Re: formalizing mathematics
Inreplyto: Your message of "Tue, 07 Jun 94 08:31:40 CDT." <9406071331.AA11087@head.cs.wisc.edu>
Date: Tue, 07 Jun 94 18:48:25 +0100
From: John Harrison
MessageID: <"swan.cl.cam.:047040:940607174833"@cl.cam.ac.uk>
Ken Kunen writes:
 If you want to verify a large chunk of mathematics, not just an isolated
 result here and there, you need to formalize something like ZFC. There's
 nothing sacred about the precise system ZFC; much weaker systems will
 suffice for most of mathematics, whereas some people might prefer stronger
 theories (e.g., Mizar adds some inaccessible cardinals for convenience).

 But to verify many of the standard results in real analysis, for example,
 we have to be able to talk about real numbers, and sets of real numbers,
 and sequences of real numbers, and functions on the real numbers..... So,
 we need a theory strong enough to construct these objects.
I think this is true; on the other hand I suspect there is a big difference
between real analysis and modern algebra in that the former requires higher
order notions mainly in a descriptive role. As such, the detailed principles
of set formation may be irrelevant. The Axiom of Choice is likely to be
needed, but either a "cumulative" set theory or a "boolean" higher order
logic would probably work equally well (it is arguable that the latter
corresponds more closely to the informal intuition in subjects like real
analysis where there are a few basic `types').
I don't know much algebra, but I suspect that the details of set theoretic
axioms are much more significant here, where one uses a lot of abstract
structures and quite complicated constructions (to justify some  often
quite simple  universal property, for example).
A useful prelude to a QED effort based on a given logic would be to look
ahead and see what resources one is likely to require in the future. For
example, what about the role of category theory? Can large categories be
an eliminable locution (a use for metatheory here, perhaps) or do we need
to tailor the basic theory to accommodate them? In the direction of
weakening ZFC, I wonder about the Axiom of Replacement. Are there any
applications in mainstream mathematics where anything like its full might
is required? Ken Kunen hinted at this kind of issue above, and maybe he
and fellow set theorists already have good answers to such questions.
John.