[FOM] Mathematics ***is*** formalising of our thought and intuition

[Vladimir Sazonov]

----- Original Message ----
> From: Robert Lindauer rlindauer at gmail.com


Dear Robert, 


Sorry for the delay and for the long reply. 


> a) I thought you were claiming mathematics was -the only science-
> creating formal tools for making our thought and intuition powerful.
>   As I said, many other kinds of scientists contribute to the effort
> in different ways, your definition turns their work into mathematics,
> which is simply not true.    

 
Sporadic, partial contributions are insufficient. 
They do not have this as their main, overwhelming and all-consuming, 
even maniacal goal. They pursue resolving their own particular 
problems and can use mathematical formalisms because the goal of 
the latter is to be potentially applicable in any activity 
of our thought. 

 
Political theory also creates formal
> models for political situations and is not -ipso facto- mathematics.

 
I know nothing about Political theory. I would rather mention instead 
jurisprudence and legislation where there is some pretension on formal 
character of their texts. My answer is that despite this pretension 
this is still rather episodic formal enterprise. Being mathematician 
and having no serious knowledge on jurisprudence (besides trying 
occasionally to read some documents which any of us sometimes read 
in our life) I just have a very strong impression that the level of 
formality in jurisprudence is incomparably lower than in mathematics 
(even in mathematics of older times of Euclid). They still crucially 
rely on the common sense (having the goal to practically resolve some 
problems between peoples like ownership, taxes, jailing etc.) whereas 
mathematicians eventually (at the final step of presentation of 
results) rely only on the mathematical rigour which, in the limit 
or in the today's ideal, is a complete formalisation (like in computer 
programming). 


Contemporary mathematics not only has the ideal of an absolute rigour, 
but this absolute is in a definite sense achievable. There is usually 
no need in mathematics to actually achieve this absolute formality, 
we have a clear feeling when a proof is completely formalisable. 
We are not just lazy to achieve this, but the strong feeling that 
a proof is completely formalisable is sufficient for our purposes. 
Mathematicians are in a sense "crazy" about pursuing the mathematical 
rigour. Even if some of them would tell that they do not need it, 
that they work exclusively intuitively, postfactum their proofs 
(if successful) are always completely formalisable. This means that 
subconsciously their intuitive style of thought is nevertheless 
directed to formalisation. The way of creating a mathematical proof 
may be highly intuitive, but the result is always (potentially) 
formalisable. Otherwise, mathematical community (unlike philosophical 
or the like) will not accept this result. 

 
Mathematical rigour is "in the blood" of mathematicians and of nobody else. 
 

> Political, Physical and other scientists use mathematics where
> appropriate and use other formalizations where mathematics is less
> appropriate 


You answer to yourself how other sciences behave: use mathematics 
(formalisations) only where appropriate. They are insufficiently 
maniacal (as mathematicians) concerning formalisation because their 
goal is different.  


The point is that formalisation of our thought proves to be so important 
thing that there exists some science which is completely devoted to 
this activity. It is called mathematics. 

 
(e.g. Linguistics has formal models of phonetical systems,
> calling them "mathematics" because available for formal modeling is at
> best a stretch - like saying that game programming -is mathematics-).

 
I already wrote on computer programming as dealing with completely 
formal objects (computer programs). This activity is in a sense 
close to mathematics (a limit case), but it is related with our 
***routine*** style of thought, unlike mathematics dealing with 
formalising our ***creative*** style thought. (This does not mean, 
of course, that programming is itself not a creative activity.)


> Meta-mathematics (both formal and informal) is not necessarily
> mathematics and yet does definitely create and use formal methods of
> consideration (e.g. Principia Mathematica).

 
Meta-mathematics is a specific kind of mathematics, like Geometry. 


> 
> b) My claim was that mathematics was not -necessarily- formal and I
> think that's borne out by the history of mathematics and even the
> dominant practice of mathematics in this century (e.g. by
> non-university mathematicians like my 10-year-old-son) - that there is
> a localization of formalization in Western Civilization's university
> system since the turn of the previous century does not overturn
> thousands of years of informal or quasi-formal mathematics!  

 
I would like to put aside the contemporary mathematical education 
which seems to me awful when even at some (or even in the majority? 
of) mathematical university departments it is considered that undergrad. 
students should not be told about rigorous proofs to not traumatise them. 
At my time we studied at school geometrical proofs on sufficiently 
detailed and rigorous level. 

 
Mathematics (for professionals) was always essentially formal 
(where the form of reasoning was more crucial than the content 
in asserting correctness of the reasoning). It always (except 
may be the time of creating of Analysis) had an instinctive 
and subconscious goal to formalise even when it was unclear what 
means a full formalisation. Otherwise what is described in the 
following paragraph would never happen.

 
The history of mathematics demonstrated the vector to more rigorous 
style of presentation of mathematical results. Recall the Analysis of 
Newton-Leibniz and its considerably later epsilon-delta formalisation. 
Before such a formalisation was achieved the situation was considered 
as unsatisfactory despite the great success of the Analysis. But note 
that the Analysis was also called the ***Calculus*** because even at 
those times (before "epsilon-delta") it was a kind of formal system 
presenting some rules of calculating derivatives, integrals and 
resolving differential equations by some kind of symbolic manipulations. 
As a formal system it was not so perfect, although highly successful 
in physics. "Epsilon-delta" gave the necessary formal foundation to 
already existing "formal building". Further foundations required 
set theory to be born, finally culminating in ZFC which gave a fully 
perfect formalisation not only to Analysis but also to all existing 
at those times mathematics. 


Which other science or human activity is so purposeful concerning forms 
of thought which it (occasionally) use. 



Nobody requires the full and actual formalisation (like in computer 
programming), but the formal ideal is currently quite clear. It could 
be discussed how this ideal can further be developed/improved, 
but in a sense it is already achieved, i.e. sufficiently well understood. 
We know what means "completely formal" and this is historically the 
greatest achievement (in particular) of Hilbert's program despite 
in some other respect it was unsuccessful (in its pretending of proving 
consistency of math). 

 

What is
> necessary is the method of abstraction by which we consider things
> without regard to their particular character  - that is, without
> regard to -what it is we're talking about at all- - this is 'almost
> formalization' in that we are considering things "formally" in the
> sense of not considering them concretely but not "formally" in the
> sense of defining method for consideration.  Other sciences do not
> completely abstract the subject-matter (neither does mathematics
> 'always'...).

 

Mathematicians sometimes (or even often) indeed do abstractions 
(generalisations) steps. But I cannot imagine a mathematician who 
permanently bears in mind that "natural numbers are abstract objects" 
and that this would help very much in creating arithmetical proofs.
In any case, it is some "acceptable methods for consideration" what 
matters in writing down final versions of proofs acceptable by the 
mathematical community. Generalisations and any other ideas and 
intuitions play a very important role on the preliminary steps. 
But you ***must*** put all your ideas into a Procrustean Bed of 
rigour. Otherwise all these abstractions will be, at beast, some 
kind of philosophy but not a mathematics at all. 

> 
> d) regarding the "guarantee" - even finite and feasible-sized proofs
> are subject to the size problem.  "The largest compact feasible proof
> is not verifiable" where compact means that any -other proof- must be
> larger than the original proof.  But this misses the point which you
> effectively make for me, much of mathematics is not feasible, making
> it unreliable, you are in the minority, as I understand it, about your
> wanting only feasible proofs about feasible mathematical objects.
> (However much I may agree with you.)  In any case, those people who
> disagree with you are -also mathematicians doing mathematics-.

 
Please ask these mathematicians to show any published paper involving  
some non-feasible proof. Who can publish in a journal an imaginary paper 
with an imaginary proof resolving some open problem? 

 
What this could ever mean? 

 
Mathematicians can deal with quite long (but still feasible) proofs. 
Long proofs are error prone, but in some way still manageable, e.g. 
by presenting proofs in a well structured form. After some attempts 
to understand and may be after some improvements making the proof 
more concise and clear it becomes confirmed to be correct. 
Otherwise the proof remains doubtful or even considered as an error. 


Non-feasible (imaginary) proofs are legal objects considered by 
meta-mathematics. But this is a quite different story. Any proof 
of a meta-mathematical theorem (about possibly non-feasible proofs) 
is still feasible. 


> 
> e) the need for formal presentation in other sciences is clear -
> without formalization, a presentation is incomplete, unconvincing and
> unclear and simply stands in need of a formal presentation.  This
> bears on the formal character of mathematics too - Cantor's system's
> formalization (zfc-ish) is not much different from the formalization
> of phonetics in that the original theories were formalizable but not
> formalized and progress in the sciences leads to this kind of
> clarification after the initial work is done.  

 

I do not know what is the formalisation of phonetics, but strongly 
suspect that this is quite different kind of formalisation in 
comparison with mathematical formalisations and with (originally 
somewhat naive) set theory. 

 
In mathematics (potential, not necessary actual) formalisability of 
the whole proof is is required with no gaps. In other sciences 
using a kind of formal steps in the whole consideration is only 
fragmentary. Experiments, some general non-formalisable general 
considerations, appealing to intuition etc. are crucially used 
in final publications in other sciences. 
In mathematics informal considerations can be also highly important, 
but the final proof is rigorous. 

 
In mathematics this
> doesn't mean that the initial work isn't mathematics (it is!), and in
> other sciences that doesn't mean that the formalizing work is
> mathematics (it isn't -always-!)
> 
> f) the formal aspects of rhetoric are as interesting as the formal
> aspects of logic, e.g. "Uses of Argument" by Toulmin.

 
I cannot judge about what I do not know. But see my comment above. 

Best wishes, 

Vladimir