[FOM] Why rigour and formalization?
Vladimir Sazonov
Vladimir.Sazonov at liverpool.ac.uk
Fri Jan 18 20:42:16 EST 2008
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.
More information about the FOM
mailing list