# [FOM] Formalization Thesis

Sun Jan 6 13:46:17 EST 2008

```Andre Rodin wrote:

> This is in accord with the view of Sazonov
> when he calls FM "tautology" (do I understand you, Vladimir,
> correctly?). But I
> don't think this view is tenable against the overwhelming presence of
> "ordinary
> mathematics".

It seems you insufficiently understand me. It seems that you as well as
many others overestimate the idea of informal mathematics. In a sense,
there is no such. However, we should be very careful and delicate in
using all such terminology. What is contemporary "ordinary
mathematics"? What means "formal"? I explain this as follows (as some
variations of what I already wrote before).

First, let me confirm that mathematical texts were always and are now
very informal, e.g. because describing the underlying intuition and
ideas. But they also always were and are containing some highly
essential formal ingredients - formal at least in a wide sense of this
word. Formal (= rigorous) in mathematics means "separating" the form of
reasoning from its content and checking correctness of the reasoning
ONLY on the base of its form. (The informal relation of form to the
content remains a very important issue.) Of course, in older times this
"detaching" and checking correctness was done instinctively,
implicitly. Only in previous century it was found a clear
(contemporary) concept of (fully) formal system and (fully) formal
proof checkable even by computer. (Also computers came into life of
everybody. Even people not related with Science nowadays feel, if not
understand, what is formal by playing with computers.) Therefore now we
achieved a NEW standard of mathematical rigour. This absolutely does
not mean that we should write down mathematical texts in this fully
formal way. But we should write TOWARDS this fully formal way. That is,
we should convince ourselves and the readers that the proof is
POTENTIALLY formalizable (say, in ZFC). At least, I personally, when
reading a text pretending to be mathematical (say, as a referee for
papers of logical character in theoretical computer science) and
struggling with the author's manner to write (a lot of authors,
including probably myself, write non-well) after understanding the
content (sometimes it is just impossible) become at the end absolutely
sure that the definitions and proofs are completely formalizable. I do
not make any real attempt to write down these
completely formal proofs. I become just absolutely sure (or almost
absolutely sure if I am a bit lazy). This is because there are already
developed some standards of presenting the material which are already
known to be acceptable. Even if some author knows nothing on ZFC and
formal logic, but uses these standards consistently (may be
instinctively) and writes sufficiently well then it is quite easy for
the experienced reader to see that the proof is completely
formalizable. This complete formalization may be awfully tedious,
non-interesting and difficult, but evidently resolvable routine task
which is, fortunately, unnecessary to do. But the very fact that it is
evidently possible is quite important guarantee of (contemporary)
mathematical rigour. I believe that at least any logician reads
mathematical texts in a similar way. Taking into account that we are
existing in mathematical community, EACH contemporary mathematical text
- the "ordinary mathematics" (does not matter how informally or
semiformally written, of course except speculations, historical,
methodological and philosophical considerations) is, after testing by
the community on its correctness, definitely CONFIRMED to be
FORMALIZABLE. Texts which are not confirmed are either nonsense or
working drafts, etc. - NOT YET MATHEMATICAL texts.

That is why I consider the Formalization Thesis (as it was formulated)
to be tautological. "Mathematical" automatically implies
"formalizable". That was essentially always the case with "formal"
understood in a wide sense of this word. Nowadays, we can say

"mathematical" implies "completely formalizable".

We should not mix drafts of mathematical texts (probably written by
"crazy" authors who are just unable to write correct proofs) from
confirmed mathematical texts which are thereby confirmed to be
formalizable according to contemporary standards.

The real closely related question here is how to do this routine work
of full formalization to be realistic. Which versions of formal
languages and formal systems to use and which kinds of abbreviations
mechanisms (definitions) to allow to make this routine process
FEASIBLE. This is, in principle, very interesting, but the mathematical
community today seemingly does not confirm the necessity to present all
mathematics in such ACTUALLY formal way, unlike POTENTIALLY formal.

Do you still consider my views as "untenable"?