[FOM] Formalization Thesis vs Formal nature of mathematics

[S. S. Kutateladze]

Sazonov    wrote :

The main definitive and distinctive attribute of mathematics is that it
is rigorous... I take rigorous = formal and understand formal in sufficiently general sense
of this word.
-----------------------------------------------
Mathematics is the pursuit of truth by way of proof  according to Mac Lane.
This definition is the alternative I prefer.


Sazonov wrote:
Mathematical definitions, constructions and proofs were always
sufficiently formal (except may be for some periods like the heroic 
time of invention of Analysis).
_______________________________________
"Formal" and "rigorous"  are time-dependent.
I appreciate "sufficiently" for reflecting the dependence on time.
The times of the invention of the calculus   were heroic indeed but not an exception since
the mathematical attributes of those days WERE "sufficiently formal"  (formal=rigorous for you).


Sazonov wrote:
Anyway, in contemporary mathematics the highest standard of rigour or
formality is known explicitly, at least to the mathematical community 
if not to each separate mathematician.
_________________________________________________

I doubt this. In my opinion, this view bases on overestimating the present state
of rigor and formalization. We all know many limitations of the today's
mathematics from  the powerful beauty of logic.


Sazonov wrote:
Nowadays it is impossible to speak on mathematical theorems and proofs
which are not (potentially) formalized yet.
____________________________________________
Some caution must be exercised while speaking so definitely.
We all remember  the claims that Cauchy and Euler were not rigorous since
they used actual infinities. The claims still sound that Archimedes had no proofs of his
formulas for volumes. Recall that Euclid had no   definition of triangle.
However his Elements has always been and will  always remain an outstanding piece
of mathematics. The continuum hypothesis is just a rephrasal of the ancient mathematical problem of
counting the points of a straight line segment.
The Goedel and  Cohen achievements are impressive but not of a greater
import as compared with the incommensurability of the the side and diagonal of a cube.
The independence of the firth postulate  would be  a trifle without
the treasure trove of the modern knowledge about various spaces of geometry.

Sazonov wrote:
I think the real question should be about the formal nature of
mathematics. Why formal side or rigour is so important in mathematics? 
_______________________________________________________________

The role of rigor and formalization is always topical for the foundations of mathematics.
However, to speak of the "formal nature"  of mathematics so definitely
is misleading in my opinion. Math is a human enterprise.


Sazonov wrote:
does the fact that a computer program (an absolutely formal text)
created by a human being can work autonomously from its creator make 
this program meaningless or something defective just because it is 
formal and autonomous?
_________________________________

Meaning is that which belongs to man.   No man, no meaning.




_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom


                
---------------------------------------------
S. Kutateladze
Sobolev Institute of Mathematics
Novosibirsk State University
            mailto: sskut at math.nsc.ru
            copyto: sskut at academ.org       
http://www.math.nsc.ru/LBRT/g2/ruswin/ssk/index.html