[FOM] Formalization Thesis: A second attempt

[Marc Alcobé]

Tim says:

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.

I think this looks a lot more like a definition of what one might
understand by "precise mathematical statement" rather than like
something that can be somehow justified. It might sound rather odd to
people who think that, for example, ¬CH is indeed a precise
mathematical statement (or PD, to give another example).

I must say I would agree quite a lot with this other definition:

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

Think about how mathematics come to existence: mathematics exist
because problems exist, and because some problems can be solved by
some specific means we call mathematical. These means involve
idealization and abstraction, i. e. as Gödel once said (see Wang's "A
logical journey"), knowing what one has to disregard. Keep the form
and forget the substance, the smile without the cat.