[FOM] Formalization Thesis

[Andre.Rodin@ens.fr]

A crucial issue about Formalization Thesis (FT) discussed in this thread seems
to be whether or not “ordinary” mathematics can be “faithfully translated” into
a formal language. I don’t think that this question and the wanted notion of
“faithful translation” should be left for an “informal” meta-mathematical
discussion. I rather agree with JS who suggested in his recent posting to
consider the case of group representations in this context. A mathematical
theory, which suggests itself for the purpose of studying “translations”
between different parts of mathematics is Category theory (CT). In particular
it suggests a precise definition of faithfulness (I mean, of course) the notion
of faithful functor), which seems to be appropriate in the given context – but
perhaps needs to be somehow specified. In any event CT clearly shows that the
issue of “translation” invoked by FT is *mathematically* non-trivial. To study
(categories of) translations between different mathematical theories (including
those called “formal systems”) is, in my view, more important than only
establish that such-and-such translation exists.

The above remark can be probably interpreted as a requirement of formalization
of the meta-theoretical discussion about formalization. But I think about it
differently. I rather suggest considering formalization as a specific
mathematical procedure in a wider mathematical (namely, category-theoretic)
setting. In this context one cannot equate “formal” with “rigorous” but can
distinguish between good and bad formalizations of a given “informal” theory.
One can be also more specific about what kind of formalization is good in a
given context. Even if CT can be indeed “formalized” by usual means as
suggested by Messing a better use of this theory for FOM, in my view, is to
apply it for specifying what exactly one means by formalization. In this latter
case one shouldn’t require formalization of CT (and the rest of maths) as a
pre-requisite.

Happy New Year!
Andrei