[FOM] Formalization Thesis

[Andre.Rodin@ens.fr]

Tim wrote:

>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
>Thesis itself.

Unless the notion of formalization and the related notion of faithful expression
(or faithful translation) are rigorously defined the Formalization Thesis
doesn’t 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. Shouldn’t one include this lack of rigor in formalization into the
total?
Arguably one shouldn’t. For it can be argued that the question of (faithfulness
of) formalization doesn’t 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
don’t think this view is tenable against the overwhelming presence of “ordinary
mathematics”.
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 shouldn’t 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 shouldn’t).
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.


Catarina asked:

->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
>mentions?

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 doesn’t solve the problem.

Andrei