[FOM] Formalization Thesis

[Vladimir Sazonov]

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"?


Vladimir Sazonov


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