FOM: ElementaryProof, ReverseMath?

[Robert S Tragesser]

        What is an elementary proof? (Below I ask if Reverse mathematics
might provide the tools for answering this question.)

        It seems to me that this is an extremely important question both
for the practice and philosophy of mathematics,  and I'm hoping that others
might share this sense.

        I was persuaded of this by Chapters 9 and 11 of Gian-Carlo Rota's
book INDISCRETE THOUGHTS(Birkhauser Boston, 1997),  where he observes,

 (1) a surprising amount of mathematics is driven by the quest for
elementary proof,
 (2) an elementary proof of a theorem shows that the theorem was
"analytically inevitable",  that it is
in some strong sense a consequence of the meaning of its terms.   An
elementary proof is therefore one that in effect emerges from the meanings
or concepts underlying the expression of the theorem;  the proof therefore
does not  "appeal to extraneous technique."
        
        That (2) suggests that implicit in the working mathematician's
conception of elemeNtary proof is an unarticulated understanding of meaning
of theorems.   THIS IS CERTAINLY SUFFICIENT TO MAKE THE NOTION OF
ELEMENTARY PROOF PHILOSOPHICALLY INTERESTING.  
        [SIDEBAR:  The notion of an elementary proof led me to suggest that
paradigm bound mathematicians (as I read Harvey Friedman as pointing out)
want an elementary proof (or disproof) of CH;  and the question is whether
or not it makes sense to look for a nonelementary proof/disproof.]

        Might Reverse Mathematics provide the tools for characterizing
"elementary proof"?  

        I've only read some expository papers about RM,  have been
impatiently awaiting Steve Simpson's book,  I ask that question as someone
who is getting interested in looking into RM,  but I am also worried about
criticism of RM to the effect that RM finds too much in theorems. . .that
the tools RM uses projects into theorems what is not there.  But this
criticism raises the question of the meaning content of mathematical
theorems::::
        My brief "survey" of (the issue of) elementary proof (reported in a
previous FOM letter) suggests that there will be a problem about
abstraction.   Can a proof of say the Fundamental Theorem of Algebra which
relies on a level of abstraction as implicit in the Gelfond-Mazur theorem
be elementary?   Well,  in what sense if any are the abstract concepts
implicit in the sense of the FTA?    
        rbrt tragesser