FOM: formalization; Tragesser

[Harvey Friedman]

Reply to Tragesser 9:53PM 6/4/99.

>        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] --

Stop complaining about f.o.m. researchers. Either express your own thoughts
on the matter or ask appropriate questions or both. There are a lot of real
problems for f.o.m. researchers to work on, rather than listen to you
inapprorpiately scold them.
>
>        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".

Stop complaining about f.o.m. researchers. Either express your own thoughts
on the matter or ask appropriate questions or both. There are a lot of real
problems for f.o.m. researchers to work on, rather than listen to you
inapprorpiately scold them.
>
>        Here I'll spell out a bit more -- and more directly -- what I am
>after

Well, that's more like it!

>        Kreisel in the 1970's called for "a natural history of
>[informal] mathematical proof" ... Here again is what must be done to make
>fom
>research fundamental science --

F.o.m. research is obviously fundamental science without "a natural history
of [informal] mathematical proof."

>to begin with a natural hbistory of
>mathematical proof ,

This seems to be a special interest of yours. I would like to see what you
have done along these lines.

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

This seems to be a special interest of yours. I would like to see what you
have done along these lines.