FOM: role of formalization in f.o.m.

[Robert Tragesser]

Steve Simpson wrote:
  >[Conway] seems to know what
  >formalization is, but he dismisses it by saying ``it seems to us
  >... that mathematics has now reached the stage where formalisation
  >within some particular axiomatic set theory is irrelevant'' and
  >calling on mathematicians to liberate themselves from the alleged
  >tyrrany of formalization.
  >I guess we could debate endlessly about what Conway meant, but I'm   
>not sure there is much point.  It's a shame that Conway apparently     
   >never clarified or amplified his anti-formalization views.


         Although of course inadequately formal,  PM was important in 
showing directly that so very much could be formalized.  Their aim and 
motive was philosophical,  foundational,  metamathematical.
        I urge that clarity or rigor demands that one be careful with 
the term "formal".  Leibniz (New Essays) introduced it to be "set out on
the basis of prior principles."  There is no commitment here to 
codifying the principles in a (privileged) logical calculus.
        One should preserve this distinction.  Instead of "is 
formalized" as it is currently used,  one should say,  for the sake fo 
precision,  "formalized and coded in a logical calculus" (or something 
like this).  Without this distinction readiuly at hand,  it is very 
difficult to distinguish between,  say,  Hilbert's formalization of 
elementary geometry in FoG (where there is no logical calculus in 
evidence)  and its subsequent (as by Tarski) presentation "formalized 
and coded in a logical calculus".  The same might be said for PM,  which
is formal,  but inadequately coded in a logical calculus.
        This would also give us a way of distinguishing the use of 
axiomatic method to do mathematics in the spirit of Emily Noether,  as 
emphasized by Herman Weyl,  where one wants to think out and write out 
the mathematical principles germane to a subject and of immediately 
value to proving strong theorems in a few pages (instead of several 
hundred pages as in PM).  But where the representation in a logical 
calculus would be of at best marginal interest fromn the point of view 
of the mathematician working within the formalization (but not the 
translation into a logical calculus).  Here in any case the aim is not 
philosophical,  fouindational,  metamathematical. . .althouigh one could
say it was foundational in the sense of extracting the really cogent and
immediately powerful/effectivew underlying or essential principles.
        It would be not unreasonable for the mathematician -- for their 
immediate purposes -- to foresee no advantage in worrying about or even 
mentioning the problem of whether the formal-principles set out could be
translated into some logical calculus.  It would be quite understandable
why they'd have no interest in that.
        It would also be reasonable for a fomer to point out that 
something interesting and even worthwhile could be learned through 
metamathematical investigations,  but,  given the extreme difficulties 
of the latter -- especially in the past two or so decades -- it would 
not be unreasonable for the mathematician to take a "show me" attitude, 
given their (the mathematician's) objectives/goals/interests.  After 
all,  it is quite possible to do some interesting mathematics,  even 
enduring mathematics,  without any concern for fom 
issues/investigations,  even when the mathematician's' concepts swerve 
toward those fom has most to say about.  It is not unreasonable for a 
mathematician to say in such a case,  given their immediate objectives 
and interests,  that they don't see any percentage just then in 
formalized-and-represented-in-a-logical-calculus not looking promising 
enough to make the perhaps titantic effort required.  This doesn't 
require that the deny the importance/value/significance of fom in 
anything like an absolute way;  nor does it require Steve Simpson's nose
to fall out of joint.
        As a sort of philosopher of mathematics,  I have only been 
curious about why fomers have not been more philosophically rigorous,  
yes even logically rigorous,  about articulating clearly and honestly 
and elaborately what is left behind when a formal-logical-calculus 
translation of a piece of mathematics is set up in place of the  piece 
of mathematics.  It doesn't seem right to dismiss the distinction 
without an elaborate and careful discussion of the difference(s);  I've 
not seen such a discussion anywhere.   This seems to indicate a 
tremendolus discrepancy in our understanding or 
intellectual/philosophical short-fall,  if not dishonesty,  in the 
thinking of fomers.

rbrttragesser
west(running)brook,  ct.