[FOM] Formalization Thesis: A second attempt

[Vladimir Sazonov]

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


Vladimir Sazonov