[FOM] Formalization Thesis: A second attempt

[Vladimir Sazonov]

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

> Vladimir Sazonov <vladimir.sazonov at yahoo.com> wrote:
> > 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. 
> 
> Let me re-emphasize that my goal in formulating the Formalization Thesis 
> is quite specific.  It is to explain why Goedel's second incompleteness 
> theorem is relevant to Hilbert's program of trying to prove the 
> consistency of mathematics.  

 
Probably it is my fault that I missed something essential in your intentions 
and arguments, but after Goedel this was discussed so many times and I do not 
see yet what is new in your formulation. One thing I would stress (e.g. in view 
of my above assertion on mathematics) that there is no hope on existence 
of one mathematical formal system which would formalise the whole mathematics, 
although I agree that ZFC indeed covers a lot of contemporary mathematics 
and that this fact is non-trivial. 

 
(It is also to explain other statements of a 
> similar nature, but let's stick to that one for now.)  In particular it is 
> not to make some grand statement about what mathematics is, in a fashion 
> that will infuriate people with opposing points of view.

 
For me, a fruitful discussion on the formal nature of mathematics 
(desirably without infuriating people!) would be more interesting. 

 
> 
> Furthermore, even if I grant your "stronger statement," what I am 
> asserting here is not tautologous or trivial.  

 
If the goal of mathematics is "to formalise" then 

        "mathematical proof" = "formal(isable) proof" 

just tautologically. But as confirmed above, the fact that ZFC covers 
a lot of mathematics is non-trivial. 


If the goal or the nature of mathematics is different, 
if formalisability is not vital for mathematics (only a desirable, 
optional feature) then there should probably exist non-formalisable 
mathematical proofs... (???)

 

Although I am not attached 
> to ZFC or to first-order logic specifically, it is important for me to 
> specify *some* particular system that has successfully captured most if 
> not all of mathematics.  It is not enough for me to make some vague 
> statement that every piece of mathematics can be formalized in some system 
> or other.  

 
Of course, you can restrict yourself if you want and as people typically do, 
but *in general* this vague statement is unavoidable. 


By the way, even the concept of a formal system both in a general sense 
(as I tried to allude in my posting) and in a more narrow sense is vague 
as well. Even in the narrow sense we should refer to languages consisting 
of finite strings of symbols in a very naive, non-formalised sense of this 
word. (Otherwise this would be a vicious circle). Only when doing 
meta-mathematics formal systems are considered as formalised (say, in PA or PRA). 


Nowadays a lot of peoples (not necessary appropriately educated) understand 
at least something on the formal nature of computers and many of them have 
at least a rudimentary knowledge on formal programming languages or can 
write and run programs without having any idea on Induction Axiom or have 
no serious knowledge on mathematical logic. They use a naive understanding 
of "formal". I refer to this kind of understanding (when I do not assume 
meta-mathematical considerations). 


Anyway, making these clarifications which are probably only tangent 
to your subject, I will follow the discussion with the interest. 



Vladimir