[FOM] mathematics as formal
Vladimir Sazonov
vladimir.sazonov at yahoo.com
Wed Mar 19 13:48:49 EDT 2008
This is my (lost - written mainly on 11th of March) reply to
Vaughan Pratt's notes on the formal nature and other aspects of
mathematics.
It seems that you understand by "formal" exactly that specific, absolute
concept which was clarified only in the previous century. Then, e.g.
Euclidean proofs in geometry (when the contemporary concept of formal
was unknown) should be considered as absolutely informal. But this is
definitely wrong. Otherwise by which miracle these old informal proofs
would be so easily and straightforwardly formalizable (say, in ZFC,
up to some encoding which is quite normal for formalization) according
to the contemporary understanding? However, Euclid used (or may be
largely invented?), instead of (absolutely) formal proofs, the usual
for all future mathematicians standards of mathematical rigour, which
means that
correctness of a mathematical proof is determined by its form - NOT
by the content (such as geometrical pictures or the like).
In general, we know the philosophical opposition of FORM vs CONTENT.
I believe, the crucial point in understanding the nature of mathematics
is that we should distinguish between the form of mathematical thought
vs its content. Only the limit case of mathematical formal thought is
embodied in the contemporary formal systems. Thus, let us understand
"form and "formal" in a wider sense. (Of course, for meaningfulness
of formal criteria of correctness we also need the content of mathematical
thought in addition to its form.)
VP:
Nature. To my thinking the nature of mathematics is abstraction of our
experience sufficient to give the abstraction an independent existence
in a mental or conceptual world. More important than formality is
simplicity of specification of the abstraction, without restriction
however on the complexity of the attendant issues and questions it
raises. Formality can serve mathematics by clarifying and
disambiguating it, and by providing a basis for the mechanization of
mathematics. These roles make formality less an intrinsic component of
the nature of mathematics than a source of ancillary services.
VS:
Your definition can be understood as that of some kind of art, say
writing fiction stories or drawing pictures. Also abstraction
(as well as simplicity, elegance, etc, what is usually ascribed to
mathematics), is not specific to it only. The most essential formal
or rigorous aspect of mathematic (distinguishing it from anything else)
you call ancillary! Is mathematical rigour an optional or absolutely
necessary requirement? It is abstract character of mathematical thought
what derivative from formality/rigour, not vice versa. Please, change
a bit your understanding of the word "formal" as suggested above, and
things will appear in completely different light.
My definition:
Mathematics is nothing else as taking and exploring the form of
human thought seriously and consistently.
Of course, form of thought has also some content - our intuition,
imagination, etc. "Taking form of thought seriously" absolutely
does not mean ignoring or neglecting the content. This only means that
it is form of thought what determines the specifics and strength of
mathematics. Mechanization you mention which is related with taking
the form of thought separately of its content is the main strength of
mathematics - mechanization and strengthening our thought! To illustrate
this, let us imagine (something highly unrealistic) that Newton laws
were formulated not in the known mathematical form - just some reasonable,
but very informal formulations (something like: the stronger is the
force the stronger is the acceleration - everything understood very
intuitively, mainly on the base of the common sense of these words).
Without Calculus developed by Newton, Leibniz and others these laws
would hardly be of so strong thought power as they are otherwise.
It is the main goal of mathematics to make our thought (and intuition)
stronger, and this is done EXACTLY by the ability to separate the form
of thought from its content and by developing the mathematical form of
thought (together with its content, of course). This way I understand
the formal nature of mathematics. In this sense mathematics was always
formal (in the wide sense) - long before the contemporary invention of
formal systems (and contemporary computers and programming languages).
Even having serious problems in rigorous proofs of the rules of the
Calculus in the time of Newton and Leibniz, they invented just a kind
of formal system (how to deal with differentials and integrals, etc.)
- fully in the line of formal view on mathematics! At last, ZFC axioms
are also non-proved - just accepted by some (good) reasons.
VP:
Practice. Formality works strongly against both the discovery and the
dissemination of mathematical results.
VS:
Just vice versa: mathematicians always worked instinctively
towards formalization (of their thought in the wide sense of
this word). The full (absolute) formalization is absolutely
unnecessary and useless during discovery and dissemination of
the results. But because mathematicians take formal aspect of
their thought seriously (even when thinking in an intuitive manner
and even if being "serious" concerning formal aspects only
instinctively, and even when their philosophical views are opposite
to formalist view on mathematics) their results prove to be always
fully formalizable (in some appropriate formal system).
As to dissemination, the typical mathematical texts contain usually
something like that: "now, after preliminary intuitive considerations
let us present the formal/rigorous definition/proof/algorithm".
The dynamics is usually and mainly from informal to formal
(at least in the wide sense of this word). Mathematical texts allow
speculations only in a very restricted and controlled way.
VP:
Foundations. This is where formality is most commonly found. However
foundations is no more mathematics than a boiler room is an office, [...]
VS:
I am not sure that I fully understand this allegory. If taking
formality (in the wide sense) seriously and consistently as I wrote
in my definition, then achieving full formality is a natural limit
point in doing mathematics. While the ordinary mathematicians do
formalization work on subconscious level and only in the wide sense
of this word, somebody (like Hilbert) can do this work fully consciously.
This is a necessary and very natural and "logical" step in developing
our general understanding of "formal". This also establishes the
contemporary (limit?) criteria of mathematical rigour. To make the
meaning of this limit understanding of the word "formal" milder,
and in the general line described above, we should understand it
rather as "formalizable".
VP:
However to say that formality is found mainly in the foundations rather
than in the nature or practice of mathematics is not to identify
formality with foundations or even to say it is the greater part of it.
Just as the infrastructure for a building is much more than the steam
it manages, so is foundations much more than mere formality.
VS:
As I argued, paying especial attention to formality is in the heart
of all mathematics, not only in its foundations. I agree with the
rest of this paragraph because foundations is a specific (new) branch
of mathematics and, as mathematics in general, it is not reduced only
to formal aspects. Besides the form of mathematical thought we also
have its content. Form cannot exist in full-fledged way without
its content (as skeleton separately of the body), and vice versa.
Concluding: The essence of mathematics is in distinguishing
between form of thought and its content with making the stress
on the form as the source of mechanization and strengthening of
our thought, but without full separation of this form from its
content. The separation is only temporary, for the sake of
mechanization of thought - the genuine goal of mathematics.
What I tried to defend above can be called the formalist view on
mathematics (or formal nature of mathematics). This is the old
brand arisen in the previous century but requiring a fresh description
(and rehabilitation).
Vladimir Sazonov
____________________________________________________________________________________
Be a better friend, newshound, and
know-it-all with Yahoo! Mobile. Try it now. http://mobile.yahoo.com/;_ylt=Ahu06i62sR8HDtDypao8Wcj9tAcJ
More information about the FOM
mailing list