FOM: formalization
Robert Tragesser
RTragesser at compuserve.com
Tue Jun 1 07:31:05 EDT 1999
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
More information about the FOM
mailing list