[FOM] Formalization Thesis

[Andre.Rodin@ens.fr]

Vladimir Sazonov wrote:


> It seems you insufficiently understand me. ... Do you still consider my views
>as "untenable"?


No, now I can see that your views are closer to my own than I previously
thought. Actually I referred to your views in order to oppose (1) the view
according to which mathematics is formal and hence the notion of informal
mathematics doesn't make sense and the issue of formalisation (i.e.
"translation into formal language") is vacuous or at least doesn't belong to
FOM and (2) the view according to which there exists "ordinary informal"
mathematics which can or can be not formalized for some reason. (Obviously a lot
depends on what exactly counts as formal but I leave it now aside.)I qualified
your views, Vladimir, as (1) but now I see that your position is subtler. When
you say

>we should convince ourselves and the readers that the proof is
>POTENTIALLY formalizable (say, in ZFC).

you apparently refer to translation into a formal language, and so your position
falls under (2). View (1) in its purest form is presented by Arnon Avron in his
posting "Natural Language Thesis" :



>they see "formalization" as a "translation" of
>"ordinary mathematics" into a formal language, rather than
>what it really is:  Expressing mathematical theorems
>and proofs in a precise, objective way, using precisely
>defined languages that have been especially *designed* for
>that purpose.


Myself I adhere to (2) but argue that the relevant notion of formalisation or
translation should be made more precise, probably through application of
Category theory. It shouldn't be an equivalence for it can be just a "one way"
translation.

best,
Andrei