| 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.