[FOM] Formalization Thesis
Andre.Rodin at ens.fr
Fri Jan 4 18:58:16 EST 2008
>Your project can be carried out, of course (or at least it can be begun).
>Whether it is "more important" is a matter of opinion, but in any case, it
>is a *different* question from the Formalization Thesis itself, which I
>consider to be interesting in its own right. Carrying out your project
>might help sharpen the discussion, but won't supersede the Formalization
Unless the notion of formalization and the related notion of faithful expression
(or faithful translation) are rigorously defined the Formalization Thesis
doesnt have any definite truth-value, and even cannot be checked against
particular examples. By making the requirement of faithfulness sufficiently
weak it is apparently always possible to make the thesis true.
This has a bearing on the issue of mathematical rigor. Allegedly formalization
brings rigor. But one should distinguish between the question of rigor in a
formalized version of a given theory and the question of rigorousness of
formalization, i.e. translation from the ordinary to the formal. It might
happen that a very non-rigorous (non-faithful) formalization brings a rigorous
theory. Shouldnt one include this lack of rigor in formalization into the
Arguably one shouldnt. For it can be argued that the question of (faithfulness
of) formalization doesnt belong to FOM and moreover to pure maths but rather
belongs to history or psychology (while FOM and the pure maths deals only with
ready-made formal constructions). This is in accord with the view of Sazonov
when he calls FM tautology (do I understand you, Vladimir, correctly?). But I
dont think this view is tenable against the overwhelming presence of ordinary
My own view is this. Having an appropriate rigorous notion of formalization in
hand one can reasonably require (on methodological grounds) from any
mathematical theory (including definitions, proves and the rest) to be
formalizable. But one shouldnt view the formalized version of a given theory
neither as essentially equivalent to its source (i.e. corresponding ordinary
theory) nor as the distilled mathematical content of this theory-source.
Successful formalization can be rather understood as a check of errors of a
particular sort (I wished to say of silly errors but probably I shouldnt).
It goes without saying that details of what counts as a successful
formalization should be a matter of possible revision: it might happen that an
apparent silly error has something more profound behind it. This requirement
doesn't make sense unless the operation of formalization is treated
mathematically in a rigorous way. CT seems to be quite appropriate for the task
but this is not a principal but rather a technical point.
->At some point, there must be a proof or an argument to the effect that the
translation procedure >provided by CT is indeed 'faithful' in the sense that we
are after here. Is there already such a >proof or argument?
The notion of functor allows for a bunch of specifications (including
faithfulness in the technical sense of CT) which could be useful in this
context. Even more importantly properties of functors can be also specified
externally. One may require, for example, for each informal theory to have
exactly one translation (of some specified type) into a fixed formal language.
In CT terms this would mean that the chosen formal system is the terminal
object in the corresponding category. The understanding of functors as
translations or transformations is, of course, a matter of informal
interpretation but it is fairly standard.
>In how much of a formalized form must a theorem of ordinary mathematics
>already be in order >to allow for the application of the techniques that Andre
The principle pre-requisite seems to be not formalization but some kind of
categorification (making into a category). Ordinary CT just like any other
part of ordinary maths is not formal. A known technique is considering formal
calculi as internal languages of appropriate categories (in particular
toposes). This provides an interesting view on relationships btw syntax and
semantics but I admit it doesnt solve the problem.
More information about the FOM