>> 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 my opinion (category theorists will probably disagree), large categories,
where they are actually useful, can be considered just a locution
in the metatheory. For example, the categories TOP and GP, of topological
spaces and groups, are just abbreviations for the formulas
TOP(x) and GP(x), and the fundamental group functor (Pi_1: TOP --> GP)
is just a defined function. The statement "Pi_1 is a functor" is an
abbreviation for a list of statements about Pi_1 preserving composition, etc.
>> .... 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').
You could formalize a certain piece of analysis using just
a few basic types: e.g., real, integer, function: real --> real.
But I think that when you really start doing analysis the way an analyst
does, the types start to multiply: we also need types for vectors
in n-space, functions: R^n --> R^m, L^p functions, etc.
Furthermore, one cannot really partition analysis off from other
branches of mathematics. The basic notions of algebra, such
as group and vector space, are frequently used in analysis.
The same theorem on vector spaces will get used in R^n and in L^p(R^n).
Certainly, our informal intuition of mathematics involves types and multiple
inheritance, but perhaps these also should be a locution in the metatheory,
not part of the formal theory.
>> 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?
Well -- it's a matter of opinion what you consider mainstream -- but
I think that at least 99% of what's in math journals doesn't need Replacement.
On the other hand, if you deleted Replacement, even "mainstream"
mathematicians might, if they thought about it, think it a bit strange that
certain "natural" constructions cannot be carried out.
For example, you need Replacement to prove that you can represent
an ordinal as a von Neumann ordinal (as the set of all its predecessors);
if you don't do this, the theory of ordinals becomes a bit ugly.
You do occasionally see infinite ordinals in mainstream mathematics,
and even in theoretical computer science.
Ken