FOM: role of formalization in f.o.m.
RTragesser at compuserve.com
Sat May 29 07:52:33 EDT 1999
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.
More information about the FOM