FOM: formalization; Tragesser
Harvey Friedman
friedman at math.ohio-state.edu
Sat Jun 5 14:48:47 EDT 1999
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.
More information about the FOM
mailing list