FOM: formalization

[Harvey Friedman]

Reply to Tragesser 7:31AM 6/1/99.

>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.)

I made some elementary points that I thought would not confuse anyone with
experience in actual formalization.
>
>        My complaint was that fom-er's are insufficiently careful in
>their talk about the very nature,  import,  utility,  and authority of
>"formalization".

Stop complaining about f.o.m. researchers. Either express your own thoughts
on the matter or ask appropriate questions or both. There are a lot of real
problems for f.o.m. researchers to work on, rather than listen to you
inapprorpiately scold them.

>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.

Stop complaining about f.o.m. researchers. Either express your own thoughts
on the matter or ask appropriate questions or both. There are a lot of real
problems for f.o.m. researchers to work on, rather than listen to you
inapprorpiately scold them.

>[[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.]]
>
>        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.

Stop complaining about f.o.m. researchers. Either express your own thoughts
on the matter or ask appropriate questions or both. There are a lot of real
problems for f.o.m. researchers to work on, rather than listen to you
inapprorpiately scold them.

>        I do not think that HF and other fom-ers fail us here

Your concerns do not rise to the level where words like "fail" are appropriate.

>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.

Your concerns do not rise to the level where words like "failure" and
"trouble" are appropriate.

>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".

Your concerns do not rise to the level where words like "fail" and
"evasive" are appropriate.

>        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 informal reasoning is conducted.]]
>
I stand by this statement.

The rest of your posting is a long winded and roundabout way of basically
referring to the legitimate question of constructing formalizations of
mathematics that are "user friendly." This is a well known problem to many
f.o.m. researchers, and one I have worked on from time to time. Why don't
you focus your remarks on this well known problem and perhaps even start
work on it rather than cast doubts on the integrity and competence of
f.o.m. researchers?