[FOM] Formalization Thesis

[Andre.Rodin@ens.fr]

William Messing wrote:
>
> 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.

Perhaps this is problematic in general but I cannot see any *specific* problem
concerning uniqueness of (co)limits in the given case. It seems that defining a
formal theory up to canonical isomorphism is perfectly fine. One may think of
such canonical isos as exchanges of symbols for different symbols. By the way,
do you now any situation where one could reasonably distinguish between
*different* terminal objects (or other (co)limits)? In other words - where the
usual identification of objects "up to canonical isomorphism" would cause a
real problem?


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

It's hardly a *complete" coincident because when people invented the term
"faithful functor" they likely had similar intuitions in their minds. But, of
course, I'm agree that any conclusion based only upon terminology would be
ungrounded. My point was different: to stress that the notion of "faithful
translation" or "faithful expression" repeatedly mentioned during the current
discussion allows for a more rigorous mathematical treatment with Category
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.


I would rather call them *equivalent* (not the same) and, indeed, consider the
choice of natural transformation you mention as a part of the data. But perhaps
I miss again your point since I cannot see any direct link between the issue of
formalisation and the problem about what counts as the "same" in categories. I
have a paper about this latter problem: http://arxiv.org/abs/math/0509596  but
I don't discuss formalisation there.

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

I mean the following. A "logical" category, say, a topos, may be viewed as a
model of its internal language. But the usual view, which somewhat "naturally"
suggests itself and motivates the terms "internal", is different: topos "comes
with" its language to begin with, or perhaps the langauge of a given topos is
"revealed" as a result of some additional effort. I think this changes
traditional views (dating back to Tarski) on relationships between formal
systems and their models quite a lot. I tried to develop this issue in this
paper:   http://arxiv.org/abs/0707.3745

Thank you very much for the interesting reference (I learnt something about
Gerbes from Larry Breen following his course in IHP last year.)

Andrei