[FOM] Formalization Thesis vs Formal nature of mathematics
S. S. Kutateladze
sskut at math.nsc.ru
Sun Dec 30 14:14:42 EST 2007
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.
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).
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.
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.
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.
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
Sobolev Institute of Mathematics
Novosibirsk State University
mailto: sskut at math.nsc.ru
copyto: sskut at academ.org
More information about the FOM