FOM: formalization

[Robert Tragesser]

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