[FOM] Formalization Thesis vs Formal nature of mathematics

[Vladimir Sazonov]

On Mon, 31 Dec 2007, S. S. Kutateladze wrote:

> Sazonov    wrote :
>
> The main definitive and distinctive attribute of mathematics is that it
> is rigorous... I take rigorous = formal and understand formal in 
> sufficiently general sense
> of this word.
> -----------------------------------------------
> Mathematics is the pursuit of truth by way of proof  according to Mac Lane.
> This definition is the alternative I prefer.
>

I do not know what is mathematical 'truth', except the truth in the 
real world. But I agree that mathematics 'plays' with 'truth', imitates 
dealing with 'truth'. Nevertheless, I consider that the goal of 
mathematics is different and more general. See below.

But please note "by way of proof". No other way to 'truth' is allowed. 
So this definition is consistent with (or is a kind of) the formalist 
view I defend.


> The times of the invention of the calculus   were heroic indeed but 
> not an exception since
> the mathematical attributes of those days WERE "sufficiently formal"  
> (formal=rigorous for you).

I would say "fragmentary formal". Epsilon-delta formalization put 
things in sufficiently self-contained way and excluded infinitesimals 
which were also "fragmentary formal" and much more difficult to 
formalize non-fragmentary. Then non-standard Analysis formalized (in a 
way) infinitesimals too.


> Sazonov wrote:
> Anyway, in contemporary mathematics the highest standard of rigour or
> formality is known explicitly, at least to the mathematical community

> _________________________________________________
>
> I doubt this. In my opinion, this view bases on overestimating the 
> present state
> of rigor and formalization. We all know many limitations of the today's
> mathematics from  the powerful beauty of logic.


I know no particular exclusion from the formalist paradigm. If you mean 
something like informal "deriving" consistency of PA, I will call this 
just a speculation which leads to diminishing the role of mathematical 
rigour and thereby wrecking the backbone of mathematics. For this 
speculation counter-speculations can be presented. Consis_PA, as a 
formula of PA, does not express adequately the consistency of PA 
because consistency should refer to formal proofs of feasible length 
whereas PA deals with both feasible and non-feasible finite objects. I 
see no way of "deriving" consistency of PA except belief. What could we 
say if it is, in fact, inconsistent? Beliefs are something outside of 
science. Science is not a theology.


> Sazonov wrote:
> Nowadays it is impossible to speak on mathematical theorems and proofs
> which are not (potentially) formalized yet.
> ____________________________________________
> Some caution must be exercised while speaking so definitely.
> We all remember  the claims that Cauchy and Euler were not rigorous since
> they used actual infinities.

I have taken such a caution into account when I wrote on Analysis.

It seems you use the term actual infinity in an ambiguous way. In the 
context of f.o.m. actual infinity assumes considering infinite sets 
(like N={0,1,2,...}) as 'existing actually, not potentially'. I think 
you mean the inverse 1/x of an "actual" infinitesimal x which is 
somewhat different idea from set theoretical infinite sets.


The claims still sound that Archimedes had no proofs of his
> formulas for volumes.

If I remember things correctly, there was some sufficiently formal 
proof, may be not satisfying the contemporary standards. At least he 
was not just an Oracle asserting Eternal Truths.

Recall that Euclid had no   definition of triangle.
> However his Elements has always been and will  always remain an 
> outstanding piece
> of mathematics.

Because he was sufficiently formal, except some minor points. The 
essence of his proofs remains the same nowadays and is essential part 
of any contemporary formalization of these proofs.


> The continuum hypothesis is just a rephrasal of the ancient 
> mathematical problem of
> counting the points of a straight line segment.

Do you actually mean that continuum has a bigger cardinality than 
natural numbers? It is not called continuum hypothesis.

> The Goedel and  Cohen achievements are impressive but not of a greater
> import as compared with the incommensurability of the the side and 
> diagonal of a cube.


I do not know what is greater. Assume so. And so what?


> The independence of the firth postulate  would be  a trifle without
> the treasure trove of the modern knowledge about various spaces of geometry.


And so what? Is this knowledge outside of the formal paradigm (or the 
paradigm of rigour) of mathematics?


> The role of rigor and formalization is always topical for the 
> foundations of mathematics.
> However, to speak of the "formal nature"  of mathematics so definitely
> is misleading in my opinion. Math is a human enterprise.


Yes, human enterprise of creating and studying formal side and formal 
tools of our thought. (Not a meaningless formal game!)

What is misleading?


> Meaning is that which belongs to man.   No man, no meaning.
>

My question was related with missing your point in your previous post. 
I still do not know what you wanted to say there.

Anyway, another man can use computer program in a meaningful way even 
without knowing the details how it works. Like we can use TV set by 
means of several buttons having no idea on radio waves, Maxwell's 
equations, etc. The crucial point is that we can distract from the 
meaning and can get a formal, in the case of mathematics, tool 
strengthening our thought. Say, Analysis (which is also called 
Calculus!), is such an extremely powerful formal tool for our thought 
concerning movement of physical bodies or the like. The goal of 
mathematics is creating and studying such tools for thought which can 
be potentially used both by mathematicians and by other people, not 
necessarily mathematicians (in which case it can be called applied 
mathematics).

Thus, the goal is formal tools, not truths. Getting truth (in the real 
world) is only a side effect of mathematical activity. 'Truth' in 
mathematics is a kind of chess piece, a very important piece, sometimes 
having relation to the truth in the real world. I would rather relate 
formal systems of mathematics with (developing of) our thought and 
intuition in a very general sense (by means of formal tools). We can 
call a theorem derived in a theory as (intuitively) true, but the main 
accent is done on derivations and derivation rules and axioms because 
they are the source of getting some formulas, algorithms and 
computations (special cases of derivations) which automate our thought.


I know that FLT was proved (to be 'true'), and know virtually nothing 
on the proof. This is almost absolutely useless knowledge. It cannot be 
used, unlike the proof and definitions, constructs and algorithms (and 
corresponding intuitions) involved in the proof.


Vladimir Sazonov


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