| 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).
Yes, that's true. I had in mind the existence of a function space
constructor, but simple dependent types like n-fold cartesian products
would also be really useful. (The lack of them in HOL has deterred me from
doing any serious multivariate analysis.)
Anyway, I just meant to suggest that we should try as far as possible to
avoid parochial assumptions about set theory. In this way we might have
theories which are more or less indifferent to the underlying formalism,
though maybe not to the extent Victor Yodaiken wants.
For example, I recently wanted to prove in HOL that for any infinite set A,
there is a bijection A x A <-> A. It was surprising how many set theory
books prove this using techniques which at least superficially seem quite
specific to ZF-style set theory (induction over alephs, or something like
that; I forget).
It took quite a while for me to find a direct Zornication proof.
(Of course the cutest proof is to apply the upward Lowenheim-Skolem theorem
to a first order theory of surjective pairing, the assertion being easy for
the special case of the natural numbers. In a higher order formalism
no metatheory is required to do this as the syntax and interpretation of
first order sentences is expressible in the object logic.)
| 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.
I think this is a very reasonable point. Type theories which are up to
formalizing mathematics seem much more complicated (to me anyway) than set
theory. HOL's type theory at least can easily be interpreted in a weakish
fragment of ZF set theory; such an interpretation is carried through in
detail in the HOL Description manual. (Mike Gordon has been looking at
practical ways of mixing set-theoretic and type-theoretic proofs in HOL.)
This might be an argument for making type theory itself just a "front end".
Perhaps in the case of constructive type theories a la Martin-Lof, this
is not so appealing to their practitioners, though!
| You do occasionally see infinite ordinals in mainstream mathematics,
| and even in theoretical computer science.
Apropos of the above points, how often are such uses really essential,
i.e. not once again locutions which can simply be eliminated in favour
of assertions about certain mappings between wosets?
John.