questions

[Harvey Friedman]

1. In a paper from 1987, Angus discusses such issues as in what fragment of
arithmetic can Falting's theorem and other classics from number theory be
proved. Chris thought that I might be able to get some seminar notes of
Angus on this topic. The natural goal is to show that all of the main
blockbuster results of number theory can be proved in EFA (exponential
function arithmetic), but Angus is not claiming anything that strong. I
would like to get into these matters here at Ohio State. I would greatly
appreciate it if Angus and any of you can get me a copy of any materials on
this topic by Angus or anyone else.

2. 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?