foundationalism and anti-foundationalism

[Lou van den Dries]

This is in response to part of an email sent by Harvey Friedman. He wrote:


 I know that the following view is very attractive to some of you sometimes:

"I don't care about what can be proved in what formal system. I only care if
the knowledge of that fact gives, as a consequence, something interesting
about the mathematics itself."

Of course, as you all know, and I often emphasize, occassionally one may
well be able to read off interesting information just from the knowledge
that something is provable in some formal system. Often this gives a new,
perhaps easier proof of a known fact, or even a new fact - which may or may
not be provable (with various degrees of difficulty) by normal methods. 

My question concerns what may be behind this disinterest. Is it 

a) the feeling that the formal systems considered are artificial or ad hoc?; or

b) even if the formal systems are completely canonical in a strong way, "I
don't give a ___ what can be proved in these systems."

In connection with b), one of my dearest friends who is among the 12
recipients of this e-mail has said 

c) we are in mathematics departments, and should be judged by the
mathematics that we do, not extramathematical issues such as "what can be
proved in what formal systems." Hence b). 

And, as you would expect, I said

d) well, we are in a University, and should be judged by the intrinsic
intellectual interest of what we do.

My question is: what do you think?

 -------------------------------------------------------------------------

Here is my response.

Formal systems and proofs in them are mathematical objects. Thus
my reaction to c) would be that what can be proved in what formal
system is obviously a mathematical issue (with occasionally interesting  
mathematical consequences outside the arena of formal systems).

Whether one cares is another thing. I do, to some extent, partly because
I have the background to appreciate some issues involved. The problem
is that life is short and mathematics is teeming with all sorts of
broad ideas of which this is one of many. And it's a matter of
individual judgement and background how much attention one is willing
to give to this particular item. And what kind of formal systems one
is willing to consider (and for what purpose). Disinterest may be a 
reasonable choice for those with other backgrounds and other horses to bet on.

On a related issue Harvey wrote:
 "Anand, now that we have growing mounting evidence of steadily higher and
higher quality that this is false on several fronts, how do we educate the
mathematicians?"

This refers to the lack of interest of most mathematicians as to what
set-existence axioms are needed to prove what theorems. 

But Harvey, you are already doing a great educational job on the
fronts where such set-existence axioms matter, like with the
Seymour-Robertson theorem whose proof exploits *necessarily* more of
the resources of ZFC than is common in mathematics. And if, as you
write, some graph theorists are taking seriously the possibility that
for their purposes they might have to go even beyond ZFC, then aren't
your educational goals well on their way of being met? And while I am
happy to hear about these matters, my main concerns lie in a rather 
different direction.     
      
                             
                              Lou van den Dries