[FOM] Formalization Thesis

S. S. Kutateladze sskut at math.nsc.ru
Sat Dec 29 12:43:46 EST 2007

Messing wrote:
I would like to see an
assertion concerning categories that can be made and proven which is not
equivalent to one expressible
It is a truism that any particular proof of a theorem
of category theory or any other branch of mathematics
is formalizable somehow. Every mathematical journal with
a decent impact factor will abstain from  publishing
a paper with a theorem that is supplied only by some informal
or unformalizable arguments that violate the up-to-date standards
of rigor. There is no much fun in explicating  truisms
as  arguments in favor of FT.

If we view FT not as morning exercises  or quibbling
then we  are to be more specific. For instance, ZFC presupposes
the classical logic, thus casting  the other trains of mathematical
thought out of mathematics. Of course, it is possible to ignore modal logic
and  the differences in the semantics of category theory and set theory.
Disregarding these matters,  the defenders of FT imply seemingly
that mathematics reduces to the texts that are meaningful
without human beings. I disagree and try to show the other 
angles  by  analogy with
the natural languages. Many texts can be translated from one language
to another, but this  cannot refute the fact that there is no grammar
for all of them.

Messing quoted Bourbaki...
Citations from classics are as informal as analogy. However,
informal does not mean  wrong or senseless.
If  citations are convincing, let us quote J. Kepler:
"And above all I value Analogies, my most reliable teachers."

Mathematics is much more than its texts and their formal
analysis---that is my simple point.

Sobolev Institute of Mathematics
Novosibirsk State University
             mailto: sskut at math.nsc.ru
             copyto: sskut at academ.org

More information about the FOM mailing list