FOM: formalization; Hilbert; Tragesser; arithmetic plus geometry
Robert Tragesser
RTragesser at compuserve.com
Fri Jun 4 21:53:19 EDT 1999
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.
More information about the FOM
mailing list