FOM: Are Harvey's postings "Foundational"?

[Richard Heck]

Here is what I take to be the foundational significance of Harvey's 
recent work. I could, of course, be wrong, but wanted to say a word so 
that it would not appear that Harvey was the only one who had any sense 
of what he is trying to do. I should say that my understanding of the 
matter benefitted from second-hand information gleaned from Warren 
Goldfarb, after Harvey visited gave a talk here last year.

Many mathematicians who do non-foundational mathematics take Goedel's 
theorem and related results to be of no real mathematical significance. 
Their reasons for this view are somewhat hard to fathom, and I'm not at 
all sure there is a coherent position that underlies it. But 
nonetheless, that is what they think. The questions set-theorists and 
the like study, especially regarding large cardinal axioms and the like, 
are regarded as fruity. One could try to convince them that there isn't 
a coherent position there, but I doubt one wouold have much success.

What Harvey is trying to do is to show that there are /natural 
mathematical problems/, that is, problems that arise naturally within 
non-foundational mathematics, that are unsolvable on the basis of, say, 
ZFC. It is even better if these problems have fairly natural-seeming 
proofs whose /formalization/ requires strong assumptions. The proofs 
that the problems in question are unsolvable are, of course, going to be 
complicated. But the problems are supposed to be simple, and natural. 
Moreover, these problems are often generalizations of yet simpler 
problems that /are/ solvable within ZFC, or PA, or what have you. That, 
too, is meant to be part of the charm.

Richard Heck