# [FOM] Formalization Thesis vs Formal nature of mathematics

Sat Dec 29 20:24:30 EST 2007

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

> 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!