FOM: formalization; Hilbert; Tragesser; arithmetic plus geometry

[Robert Tragesser]

        It was Harvey Friedman who used the expression "unprecedently 
[sic.] careful" and spoke of/introduced "seeming necessity", as in 

[[Harvey Friedman wrote:  A full formalization of mathematics or an area
of mathematics seems to necessarily involve a logical calculus - or 
equivalent.]]

        As was easy to predict,  Friedman,  though hardly a master of 
evasion,  in his mindless iteration of "Don't complain about fom 
researchers. . ." certainly proves himself blindly relentless at it,  
preferring to speak _ex cathedra_ rather than working out something that
must be very hard for him,  . . .providing the sort of natural history 
of informal proof called for by Kreisel and Rota [see the paragraph 
after the next] --

        Raising a fundamental problem for fom investigators must count 
as a thought,  even if it evokes thoughtless responses.  Since Friedman 
was being "unprecedently careful" I supposed it apt to use his own 
phrasing to raise the problem that bothers me.  Friedman clearly could 
not mean that it is simply analytic of what "full formalization" means 
that it "involves a logical calculus".   It is reasonable not to take 
Friedman's word for it [his _ex cathedra_ pronouncements may amuse,  but
they don't impress],  but top ask him for an "unprecedently careful" 
explanation of that non-trivial [because not trivially analytic;  though
Simpson tries to evade the problem -- implicitly raised by the 
apparently further seeing Friedman -- by making "involving a logical 
calculus" analytic of "full formalization".

        Here I'll spell out a bit more -- and more directly -- what I am
after
        Kreisel in the 1970's called for "a natural history of 
[informal] mathematical proof" (soemthing Lakatos,  say, attempted to 
begin,  but his attempts were ruined by his crippling ideology]  This 
means of course not a history of mathematical proof in the usual sense, 
but careful observatiuon and descriptiuon of (informal) mathematical 
proof,  salient features noticed,  articulated,  organized.   This was 
to be preliminary to a kind of authentic or genuine theory of "natural 
occurring" mathematical proof,  a less scientifically naive proof theory
than that actually practiced.  Such a natural history of (informal) 
mathematical proof.  Here again is what must be done to make fom 
research fundamental science -- to begin with a natural hbistory of 
mathematical proof ,  describing carefully the operations,  somewhat 
"dialectical" in character -- that legitimately lead from informal proof
to its "formalization",  remarking at each point of what has changed,  
what has been left behind,  an full evaluzation of what has been left 
behind,  the legitimacy of those changes,  the sense in which the 
changes do and do not preserve identity of proof.

rbrt tragesser
west(running)brook,  ct.