# [FOM] Formalization Thesis: A second attempt

Sat May 22 15:52:26 EDT 2010

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

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