# [FOM] Formalization Thesis

messing messi001 at umn.edu
Sun Jan 6 09:33:32 EST 2008

```Rodin wrote:

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 haveexactly 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.
--------------------------------------------------------------------------

I do not understand.  A category which possesses a final object, does
not necessarily possess an unique final object.  For example, any one
element set, is a final object in the category of sets.  Any inverse
limit (or for that matter any direct limit), if it exists, is defined
only up to canonical isomorphism.  I continue to be perplexed by the
idea of using category theory to formulate the Formaization Thesis.  The
fact that faithfullness of a functor is a concept of category theory is,
it seems to me, a linguistic coincidence with the idea of seeking a
"faithful translation " into ZFC (or any other formal theory).  Also,
since the notion of ismomorphism betweeen categories is (obviously) too
strict for any serious mathematical use, are two formalizations,
expressed in the language of category theory to be regarded as "the
same" if the categories are equivalent, and if so, is a specification of
the equivalence between the two categorries to be considered part of the
given data?  If C and D are categories and F:C ---> D is an equivalence,
is the choice of a quasi-inverse G:D ---> C to be part of the given
data.  If so, is the choice of a natural transformation t:GF ===> Id_C,
which is such that, for every object, c, of C t_c:GF(c) ---> c is an
isomorphism, to be part of the given data.  Such specifications are
frequently necessary in actually using category theoretic notions in
other areas of matiematics.  See, for example, my paper with Larry
Breen, The Differential Geometry of Gerbes, Math ArXiv math.AG/0106083.
-------------------------------------------------------------------------

Rodin wrote:

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

Can one be more explicit about the "interesting view on the
relationships between syntax and semantics" provided by the use of
category theory?

William Messing

```