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

*To*: Blind.Copy.Receiver@compuserve.com*Subject*: RE: FOM: formalization*From*: Robert Tragesser <RTragesser@compuserve.com>*Date*: Tue, 1 Jun 1999 07:31:05 -0400*Sender*: owner-fom@math.psu.edu

Reply to Harvey Friedman. HF's remarks are clarifying and forceful, but his twice told [[HF: It is not easy to talk about formalization in a clear way. Unless one is almost unprecedently careful, one is surely going to be misunderstood. I will attempt to be that careful.]] is something of a teaser; it certainly raised my hopes, but he didn't deliver on it. (Maybe this is unfair, for he did say only that he would "attempt", and he did deliver an attempt.) My complaint was that fom-er's are insufficiently careful in their talk about the very nature, import, utility, and authority of "formalization". I do not have an explanation for this insufficiency; that I am not mistaken that there is such an insufficiency is evidenced by HF's saying that he was going to be "unprecedently careful". My suggestion of a kind of intellectual "dishonesty" might better have been a pointing out of a sense of evasiveness I have that is simply heightened by HF's promising, but not delivering on, talking about formalization in an unprecedently careful way. At the same time, perhaps the fault is not his, but only mine in not making what worries me sufficiently plain. There is one remark in particular I might address that might help to make my problem (a problem of understanding and appreciation) clearer. Harvey Friedman wrote: [[HF:The quest for formalization - in the relevant sense here - arises whenever there is an intellectual development in which the underlying assumptions have not been clearly identified. Often there is unclarity about what the underlying undefined concepts are.]] He goes on to say about formalization in relation to logical calculi: [[HF: A full formalization of mathematics or an area of mathematics seems to necessary involve a logical calculus - or equivalent. So your distinction appears to be based on a confusion.]] It is exactly the "seems to necessarily involve" that troubles me and gives me a sense that I am in the presence of evasions. "Seems to involve"--alright. "Necessarily involves"--alright. But "seems to necessarily"; oxymoronic or evasive, take your choice. But what is being evaded? HF would not want to settle for "seems to involve", for that would be too weak. But his scientific integrity prevents him from outright asserting "necessarily involves", for then he would have to give a demonstration of that necessity, and in order to do that he would indeed have to talk about "formalization" in an "unprecedently careful" way. Let me say that I AM NOT INTERESTED IN CHALLENGING THE CLAIM TO NECESSITY, I AM RATHER EXTREMELY WORRIED ABOUT THE ABSENCE OF A SERIOUS "UNPRECEDENTLY CAREFUL" DEMONSTRATION OF IT. I do not think that HF and other fom-ers fail us here because they are here out of their depth; G-C Rota once suggested that the failure has more to do with their grammatical or descriptive or characterizational powers, and I am certain that this is where the trouble lies. Where do their powers fail them? In characterizing informal mathematics and informal proof, and in observing and describing the (presumably rational) process of formalization itself. Only with such characterizations and observations at hand could they be able to substitute "necessarily involves" for the evasive "seems to necessarily involve". The following remark of HF helps me to make my point: [[HF: You are confusing informal proofs with formal proofs. The latter is what is relevant when discussing formalization. An important project is to redesign the axioms and rules of logic so as to be closer to the way informa reasoning is conducted.]] I of all people am not confusing formal and informal proof. Perhaps HF's attribution of "confusion" comes from his own rather haphazard uses of the expressions 'full formalization' and cognates of 'formal' unmodified by 'full'. I suggested that one make "to formalize" mean [I'm more explicit now} "the process of uncovering and articulating and recasting a subject matter according to its first or essential or most central principles" [by his earlier remark above, HF would seem to concur]. This is how Leibniz used the term; but of course this process was first discovered by Plato (on at least Bill Tait's reading of Plato or moy reading of Bill Tait's reading]. There are then various extents of "formalization". It is not implausible that "full formalization" of any subject matter would involve logical principles, and that those logical principles can be resolved into a logical calculus sufficient to as it were "calculate" any genuinely logical implication. Now we come to what I think is the central issue. Harvey Friedman does clearly admit that there is something different about "informal reasoning", and that it is some sort of deficiency of logical calculi that they do not sufficiently close with "informal reasoning". Now I think I can say exactly what troubles me.-- There is a difference between informal reasoning/proof and _fully [sic.] formal_ such. In order to see why fully formalized reeasoning "necessarily involves" first order classical logic with identity (this or any logical calculus), we need to understand the informal and the rational process of formalization much better than we do. And I suspect with Rota that fomer's simply do not have the powers of observation and description to realize such an understanding. That informal reasoning is significant is clearly acknowledged by Friedman, if rather meagerly, in his observation that it is an important task of fully formal logic to attempt to close in on it. But until we have adequately and richly observed and articulated the informal and the ratiuonal processes of formalization, the claim that "full formalization necessarily involves articulation within the classical first order logic with identity [or any logical calculus]" is without genuine scientific support (N.B.: however credible it might otherwise be). It is this absence of scientific support (not credibility) that I perceive as the (not so concealed) hole beneath the foundation of fomer undertakings. sincerely and in gratitude rbrt tragesser west(running)brook, ct. usa

**Follow-Ups**:**Harvey Friedman**- FOM: formalization**Stephen G Simpson**- FOM: role of formalization in f.o.m.

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

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