# [FOM] Formalization Thesis: A second attempt

Wed May 19 19:07:12 EDT 2010

```----- Original Message ----
> From: Timothy Y. Chow tchow at alum.mit.edu

................
> Back in December 2007, I proposed something that I called the
"Formalization
> Thesis" that generated a lot of
> discussion.

http://cs.nyu.edu/pipermail/fom/2007-December/012371.html

With
> the benefit of the feedback from the first FOM discussion, let me now
>
propose what I think is a better statement of the Formalization
> Thesis:

Given any precise mathematical statement, one can exhibit
> a formal
sentence S in the first-order language of set theory with
> the property
that any mathematically acceptable proof of the original
> mathematical
statement can be mimicked to produce a formal proof of S
> from the axioms
of ZFC.

As I said in my original FOM post, my
> focus is not so much on ZFC
particularly; that is, I will not quibble with
> someone who wishes to
replace "ZFC" with another system that is somewhat
> weaker or stronger.

I would also omit the implicit use of first order logic here.
Formalisations can be of ANY kind. ZFC is potentially not unique
preferable one and we do not know which formalisms could be used
in the future. Even now we have e.g. NF which is (probably) incomparable
with ZFC.

But my main disagreement is with the status of your Thesis as "thesis",
i.e. as a kind of a neutral observation. I would prefer to replace this Thesis
by something relevant and stronger what explains the nature of mathematics:

Mathematics ***is*** formalising of our thought and intuition.

Mathematics also deals with (or studies) any such formalisms
just by doing formal derivations or by using other formalisms
(that is mathematics is also its own metamathematics).

It is also necessary to explain WHY do we formalise at all.
Because formalisation is a kind of organisation, mechanisation, automation,
and therefore effictevisation, acceleration, strengthening of our thought
and intuition. In this sense mathematics is a kind of engineering activity
creating formal tools strengthening our thought. This automation is quite
an important fundamental problem for humans. That is why mathematics has
arisen and became the "Queen of Sciences" (as well as a universal servant).

*From this point of view* your Thesis is just a tautology (as I already
wrote in the former discussion), so for me there is almost nothing to
discuss in this Thesis. This is another reason why I am not satisfied
with your Thesis and present some relevant and stronger alternative.

To be applicable to older times, the word formal should be understood not only
in the most narrow contemporary sense. It can also be understood in that sense
that Euclid proofs were also quite formal (rigorous), i.e. formal enough to
sufficiently easily distinguish whether a reasoning is correct, i.e. follows
some explicit or implicit canons. Formal in a wide sense of this word means that
the form is prevailing (and even is vital) over the content of our thought WHEN
we consider its correctness. For example the correctness of a geometrical proof
is determined not by geometrical figures drawn on a paper but rather by the form
of reasoning. Euclid presented these forms or templates of reasoning by numerous
examples so that other people were able to follow them even without having full
(contemporary) formalisation. In other situations (such as considering the meaning
of our formalisms) the content (or intuition) of our mathematical thought is prevailing.
The contemporary (narrow) meaning of the word formal is a limit goal of
contemporary mathematics (usually still unconscious) in comparison with the times
of Euclid and later times when only a rigour was required. That is, rigour is a
synonym of formal in a weaker sense (semi-formal).

If we will present a "mathematical" proof which is doubtful to be potentially fully
formalisable (in a suitable formal system, possibly created especially for this proof
or for a class of such proofs) then it will not be accepted as true mathematical.
(However it can be accepted as a draft of a possible, hopefully successful proof.)

The last paragraph can be considered as a replacement of your thesis in the form
which I would accept it as a thesis on our contemporary mathematical community.
This is just an observation, a reflection, but I prefer some explanation of what
is mathematics like that I presented above and which I would call

a (renewed) formalist view on mathematics.

It is renewed e.g. because it *explicitly* asserts that the "play with formulas"
is quite meaningful: We formalise to make our thought powerful.

```