>> 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?
BUT: Most mathematicians use types and will reject ill-typed expressions.
Ken Kunen wrote:
>> 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".
Recall Paul Halmos's nightmare of a mathematician from his paper "How to write mathematics": A sequence epsilon_n that tends to infinity if n tends to 0.
The advantage of set theory is, that it enables a typed language with quantifiers "for all X in Y ..." and "for some X in Y ...", but it does not enforce it. Many things in mathematics can be expressed by Delta_0-formulas, i. e. using only these bounded quantifiers, but some - like the existence of a power set - cannot.
A major advantage of types for proving theorems in Mathematics is, that they help chosing the knowledge to use in order to prove a specific theorem. In order to prove a theorem on real numbers, in the first run only knowledge on real numbers will be used. This is a concious strategic decision of the prover - it is not enforced by the logic and it can be wrong. E. g. in order to prove the intermediate value theorem for polynomials - a statement that involves only numbers and arithmetic operations - it is necessary, to consider the reals as a set, either using properties of it's subsets or properties of the real numbers themselves as sets.
In order for a QED project to attract mathematicians it should - like set theory - support the use of types but not enforce it.
Ingo Dahn