# [FOM] Formalization Thesis

messing messi001 at umn.edu
Fri Dec 28 08:46:58 EST 2007

```Concerning Kutateladze's comments about category theory and elementary
toposes, I think he is mistaken.  In ZFC a category is defined as an
ordered sextuple: C = (M, O, s, t, c, i) where M and O are sets (the
morphisms and objects), s:M --> O, t: M: --> O are the source and target
maps, letting M* denote the fiber product of M with itself over O
relative to the maps s and t, c:M* --> M is the composition map and
i:O --> M is the map assigning to each object its identity morphism.
This is an "algebraic structure" in the sense of Bourbaki in that it is
defined in terms of finite inverse limits and subject to some axioms.
As an elementary topos is a category subject to some additional axioms,
it is obvious that the concept of an elementary topos is faithfullyu
represented in ZFC.

As someone who uses the "cohomological machine" in my everyday
mathematics, I would personally prefer to state the Formalization Thesis
in ZFC + Grothendieck's axioms for universes.  This because, as is well
known and as I discussed in the thread concerning FLT, as soon as one is
led to consider, for two categories C and D, the category HOM(C, D)
whose objects are the functors F:C --> D and whose morphisms are the
natural transformations between two such functors, size issues
immediately come in to play.  Needless to say this is even more true if
one looks at higher category theory, as is increasingly being done by
topologists in connection with homotopy theory and stable homotopy theory.

Finally I do not at all understand Kutateladze's statement: "Hieroglyphs
are not letters, that's the point."  A hieroglyph is a written
character that functions as a symbol, a has exactly the same function
and use.  The fact that hieroglyphs are most often pictorial is entirely
irrelevant to the question and is, nothing but an historical
circumstance.  I thought it is well known that letters can be
represented by the use of precisely two symbols, say x and ', where the
n^th letter is x followed by n  repetitions of the symbol '.  I do not
worry here about alphabets which have more than a countable set of letters.

William Messing
```