[FOM] Formalization Thesis vs Formal nature of mathematics

[Vladimir Sazonov]

The question discussed so far is whether any mathematical theorem and 
its proof can be formalized, say, in ZFC. It appears as if 
"mathematical" is something which exists and makes sense independently 
of any formalization and can be (optionally?) formalized. I understand 
things differently.

The main definitive and distinctive attribute of mathematics is that it 
is rigorous. But what means rigorous needs to be explained. I take 
rigorous = formal and understand formal in sufficiently general sense 
of this word. The contemporary concept of formal system (FOL, PA, ZFC, 
etc.) is only a limited version of 'formal'.

Mathematical definitions, constructions and proofs were always 
sufficiently formal (except may be for some periods like the heroic 
time of invention of Analysis). In a rigorous/formal proof (or 
construction or definition) we deliberately distract from the content 
(intuition) and check only correctness of the form of the proof 
according to some standards - depending on the historical time, of 
course. These standards can be known either explicitly, like in 
contemporary formal systems where even computer can perform this 
checking, or invented and used instinctively and studied just by the 
way of training in doing/reading/repeating mathematical proofs under 
supervision of experienced mathematician/teacher as it was always the 
case, and is also in our time. Of course, we additionally adapt these 
standards to our intuition, and vice versa. (Not a meaningless formal 
play!) The 'vice versa' is also important because our intuition can be 
considerably changed by formalization. (E.g. the counterintuitive and 
non-intended to be deliberately introduced by the epsilon-delta 
formalization continuous and nowhere differentiable curves become quite 
intuitive after some experience in doing formal proofs in Analysis.) 
Thus, when we say that a formalization of our intuition is adequate or 
faithful, we should realize that this is understood in not so 
straightforward way.

Anyway, in contemporary mathematics the highest standard of rigour or 
formality is known explicitly, at least to the mathematical community 
if not to each separate mathematician. This is the result of the 
progress done in foundations of mathematics in the previous century. 
Nowadays it is impossible to speak on mathematical theorems and proofs 
which are not (potentially) formalized yet. A "proof" which is doubtful 
to be formalizable (in some formal system) is not considered as 
mathematical. It is only a draft of a possible mathematical proof, if 
any. Of course, mathematics (unlike programming or software 
engineering) does not require completed formalization (like a computer 
program). We need only potential formalizability. The point is that 
mathematicians can usually clearly distinguish potential 
formalizability from irresponsible speculations and are highly 
sensitive in this respect.

Now, on Formalization Thesis. I understand that only intuition, or 
preliminary considerations or drafts of proofs can be formalizaed, that 
is, made mathematical. Mathematical proofs (if they are really 
confirmed by mathematical community) are already formal(izable) in a 
formal system. This formal system may be not mentioned explicitly in 
the proof. But understanding and confirming a proof assumes convincing 
ourselves that some formalization is possible, and this is possible 
only if the author of the proof acts according to the standards of 
rigour, i.e. sufficiently formally.

Then, what is the content of Formalization Thesis? To show 
formalizability of what is already shown to be formalizable? Or to 
transform formalizable proof to explicitly/absolutely formal (like a 
computer program)? The last task is quite interesting in itself, but 
potential formalizability is usually quite sufficient for mathematical 
rigour. It would be awful for mathematicians to write absolutely formal 
proofs. But it is compulsory to be convincing that the proof is 
potentially foprmalizable.


I think the real question should be about the formal nature of 
mathematics. Why formal side or rigour is so important in mathematics? 
How it woks for strengthening our intuition and thought because formal 
systems for our thought are like mechanical and other engineering tools 
and devices making us stronger faster, etc.


BEZIAU Jean-Yves wrote:

> Formalization, what a nasty world !

Cars, air planes, computers -- what a nasty world?

Can you imagine mathematics without rigour?


S. S. Kutateladze wrote:

> the defenders of FT imply seemingly
> that mathematics reduces to the texts that are meaningful
> without human beings. I disagree

I am defender of a formalist view on mathematics - not of FT as it was 
stated. Anyway, it is difficult to understand what do you mean. Say, 
does the fact that a computer program (an absolutely formal text) 
created by a human being can work autonomously from its creator make 
this program meaningless or something defective just because it is 
formal and autonomous? (Note that such a program can involve a lot of 
original ideas probably also from mathematics and do something very 
useful.)


Happy New Year to everybody!

Vladimir Sazonov



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