[FOM] Why rigour and formalization?

[Vladimir Sazonov]

It seems there is opinion that mathematicians are so pedantic in using 
rigorous proofs because they care about precision of their results and 
also about reliability of their proof. The latter means that if A is 
rigorously proved then it is definitely true. This also would mean that 
it is the truth which mathematics is pursuing. But why physicists who 
are also pursuing truth use so different methods? (Even if they also 
use mathematics they neglect the rigour in proving mathematical 
results.) Precision is also what is highly important to them. Why so 
different approaches? Also why the "visual" proof presented by Bill 
Taylor is considered as mathematically problematic despite it seems so 
intuitively convincing? Why do we so scrupulously prove that any 
continuous curve going from one side of the axis to another must 
intersect it - intuitively so evident fact? It might seem even 
ridiculous.

I see the answer in realizing that:

(FVM) The subject matter of mathematics is tools "automating" and 
strengthening our thought and intuition. Quite naturally, such tools 
have the form of contemporary formal systems which embody mathematical 
rigour.

It follows from this formalist view on mathematics (FVM) that 
mathematics is not about truth and even not about precision, at least 
not at the first place. It is about "automation". This automation is 
based on making these tools of thought of formal systems and is closely 
related with computations, nowadays even with potential using 
contemporary computers. This "automation of thought" can be considered 
both as subject matter and methodology of mathematics. That we 
typically use formal systems to derive some "truths" and seemingly care 
too much about whether mathematical statements are true or not 
(actually, provable or disprovable), is not the most important thing. 
Yes, we care, but we mostly care to present rigorous proofs. Otherwise 
mathematicians would behave more like physicists. But this is 
definitely not acceptable for them. They have different goals - 
absolutely not because of pedantry or bureaucracy! Is automation a 
pedantry?

Taking that formal is related to mathematical intuition as form to 
content (in the general philosophical sense) and that the goal of 
formal tools is "automation" of thought, it is imaginable that the 
specific mathematical form of our thought could have some more general 
character than that based on formal languages (sets of strings in an 
alphabet) and formal systems in the traditional (narrow) sense of the 
word "formal" in f.o.m. As the main (and first) users of such tools are 
human mathematicians (not necessarily computers) these formal systems 
could have in some cases somewhat more convenient, user friendly form. 
For example, diagrams in category theory. Of course these diagrams are 
quite discrete objects and can be symbolically encoded. But we prefer 
to use them visually. The visual proof presented by Bill probably could 
be also considered in a way as one of many such kind of proofs based on 
a similar system of visualized diagrams. Anyway the general term "form" 
or "formal" could mean also something of geometrical or graphical 
nature. The main point is the ability to use such graphical proofs and 
such kind of graphical formal system as tools making our thought 
stronger. They could be translatable (encodable) to traditional formal 
systems using languages in a finite alphabet and therefore also having 
computer implementation.

By the way, if truth is not the main goal for mathematics, the (highly 
doubtful, in my opinion) Platonist views on its nature and especially 
on the "absolute mathematical truth" can be easily avoided. We have 
various mathematical intuitions supported by formal tools, and that is 
all what we need. We can imagine various mathematical worlds satisfying 
that or other system of axioms referring to our intuition without any 
need of a (unified and uniquely existing) world of mathematical 
objects. Our mathematical intuition is (honestly speaking, without 
opinionated pretension on anything more like absolute truth) quite 
vague, but nevertheless, being supported by a formal system and due to 
this support, proves to be extremely strong. This is the point of 
mathematical rigour and formalization.

Finally, consider two questions posed by Vaughan Pratt:

1.  Can mathematics be formalized?

2.  Is there a universal mathematical framework?

My answers:

1. As science on various formal systems mathematics, in general, has no 
intension to be concentrated on one of them. However, some formal 
systems like ZFC could *currently* serve as universal ones which can 
interpret the most of typical formal systems. Anyway, the ability to 
interpret various formal system in one of them does not diminish the 
role of each of these formal system and does not reduce mathematics to 
one of them.

2. A very general framework sufficient for the contemporary and 
hopefully for the future vision of mathematics: Inventing and studying 
various formal systems serving as tools of strengthening thought.


Vladimir Sazonov

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.