[FOM] Formalization Thesis

[messing]

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