[FOM] Formalization Thesis

[messing]

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