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

*To*: Blind.Copy.Receiver@compuserve.com*Subject*: FOM: formalization; Hilbert; Tragesser; arithmetic plus geometry*From*: Robert Tragesser <RTragesser@compuserve.com>*Date*: Fri, 4 Jun 1999 21:53:19 -0400*Sender*: owner-fom@math.psu.edu

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.

**Follow-Ups**:**Harvey Friedman**- FOM: formalization; Tragesser

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

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