[FOM] Formalization Thesis vs Formal nature of mathematics

[Vladimir Sazonov]

S. S. Kutateladze [mailto:sskut at math.nsc.ru] wrote:

> Sazonov    wrote :
>
> Mathematical proofs  are always sufficiently formal (just
>
> to such degree to which it is necessary/essential).
>
> Otherwise they are not mathematical.
>
> ___________________________________________
>
> I appreciate that you use the words "sufficently" and "necessary" in 
> regard to proofs so informally.

For example, proofs for infinitesimals at the "heroic time" were 
"insufficiently" formal to the "necessary" degree. They were rather 
"fragmentary formal", and it was unclear at that time how to make 
"fragmentary formal" to be "formal" - even in the wide sense of this 
word which we already discussed. These were not just several minor 
"gaps" in formalization.


This was the lack of rigour (the lack of
>
> mathematics in these considerations).
>
> _________________________________
>
>
>
>
> I disagree that there was any lack of mathematics in
>
> the  mathematical discoveries of Newton, Leibniz, and other 
> forefathers of the calculus.

I think, there is no need to defend from me these great mathematicians. 
Also, as I wrote, drafts of proof or "fragmentary formal" proof can 
have high mathematical value. But if there would be no essential 
defects in the rigour of Analysis, realized already at that time, 
mathematicians would not have to invent the radical remedy - 
epsilon-delta formalization - and Nonstandard Analysis would not be 
considered as so crucial point in formalization of actual 
infinitesimals. At least in my time students in math were told 
explicitly that infinitesimals are not rigorous (although just at that 
time it was published the book of Robinson) and we were required to 
follow the standards of rigour based on epsilon-delta. Lack of rigour - 
the definitive feature of mathematics - is the lack of mathematics (by 
definition). In comparison, nothing similar was in the case of 
Euclidean Geometry - the template of mathematical rigour virtually till 
nowadays. Omissions (or gaps) like implicit use of Pasch's axiom were 
just a minor drawbacks (noticed only two thousands years later) in 
comparison with the blatant lack of rigour concerning infinitesimals.


> You see all of mathematics from a formalists
>
> point of view. I do not doubt this, but this does not exclude other 
> views of the whole of mathematics.


which do not seem to me convincing. Recall, for example, "mathematical 
realism" having no relation to the realist view in the normal sense of 
this word.


> However, I'll add an argument in favor of formalism at this point. We 
> often end a proof with claiming "obvious." However,
>
> we abstain from refer to the Indian pictures  of the Pythagorean 
> theorem as proofs. The reason is that "obvious"
>
> is personal or subjective. Mathematics starts with  a quest
>
> for  more "impersonal" or objective proofs.


If we both agree at this point, what is the serious reason of quarrels 
in other much less essential issues?

If mathematics starts here, as you write, then the lack of rigour is 
the lack of mathematics.

>  Sazonov wrote:
>
>  We have reached a kind of absolute rigour,
>
> at least a "stable" point. _______________________________________________
>
> I doubt this. We are not smarter that our ancestors.
>
> Please note that the drastic twists and turns  of the
>
> mathematical views of foundation in the twentieth century.
>
> I do not think that this will terminate ever.
>


The question is not whether we will terminate and whether we are 
smarter. Contemporary standard of rigour assumes (potential) 
possibility to check proofs by computers (a dream of Leibnitz). In a 
sense we eventually achieved this dream. What will happen with 
mathematical rigour later, we do not know, but at this state of affairs 
we have a "stable limit" point. It is stable because we can only 
fantasize on the future. To move from this point some serious force (of 
unknown nature yet) should be applied.


Best wishes,

Vladimir Sazonov


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