| Did I miss something, or is this just a not so wonderful re-explanation
| of how everything can be encoded in sets?
I thought its message was really "Types considered unnecessary". The
argument that types get in the way of mathematics is, in my view, true in
certain cases (one Javier Thayer and I discussed was finding the algebraic
closure of a field) but there is no supporting evidence given in this
paper -- it's merely stated as a fact.
The discussion of undefinedness is far too offhand -- I believe that a
more elaborate treatment of undefinedness (as in IMPS) is implicit in many
mathematical notations and habits.
Riemann integration is something that can just as well be done in simple
type theory (it has, in a slightly different form, been done in HOL). And
as I never tire of saying, lambda calculus provides a good way of dealing
with variable binding constructs.
The final remark about mathematicians having "gotten along" without types
for 2000 years might equally be applied to sets.
But the paper was quite a good read, and the topic merits discussion. I'm
an agnostic on the question, though I am much more familiar with formal
proofs in type theory than set theory. It may only be when we push
formalization into more complicated parts of mathematics that we have the
perspective to decide the issue.
John.