[FOM] Formalization Thesis: A second attempt

[Timothy Y. Chow]

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

Furthermore, even if I grant your "stronger statement," what I am 
asserting here is not tautologous or trivial.  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.  I want to be able to say that *any* proof of the consistency of 
mathematics that someone might come up with can be imitated in *one* 
particular system, to which Goedel's second theorem applies.  Only then 
can I reach the desired conclusion that Goedel's second theorem rules out 
the possibility of a mathematical proof of the consistency of mathematics.

The fact that a *single* system suffices for most if not all of 
mathematics is not at all trivial, and we can feel confident of it only 
because people have put in a lot of work to verify it.

Tim