[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: formalization; Tragesser*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Sat, 5 Jun 1999 19:48:47 +0100*In-Reply-To*: <199906042153_MC2-783B-500C@compuserve.com>*Sender*: owner-fom@math.psu.edu

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.

**References**:**Robert Tragesser**- FOM: formalization; Hilbert; Tragesser; arithmetic plus geometry

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]