>> Since the teaching of Bourbaki very many pure mathematicians feel that
>> they should think that all their objects are untyped sets, but what
>> does that really mean for them?
What it means is that we understand:
1. All of standard math can, in theory, be formalized within ZFC.
2. Doing so would be extremely painful in practice.
The importance of (1) is that to prove an independence result, such as:
CH is independent of "standard mathematical reasoning" ,
we need only produce a model for:
ZFC + not CH,
which is a fairly simple theory in ordinary untyped predicate logic.
This is a lot easier than working with models for a logic with
some complex type structure.
Fact (2) doesn't bother mathematicians, since in practice they
never formalize anything, so they are happy to be aware of (1)
and continue to think informally in terms of types.
Even books (such as mine) on pure set theory often use typing to facilitate
the exposition. For example, borrowing from Fortran, we say:
"we use Greek letters alpha,beta,gamma ... to vary over ordinals".
Ken Kunen