[FOM] mathematics as formal

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