[FOM] Formalization Thesis: A second attempt
Timothy Y. Chow
tchow at alum.mit.edu
Fri May 21 17:11:17 EDT 2010
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 ***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.
More information about the FOM