[FOM] Formalization Thesis

[messing]

Andrei Rodin wrote:
 > >To study (categories of) translations between different mathematical
 > >theories (including those called "formal systems") is, in my view, more
 > >important than only establish that such-and-such translation exists.


With regard to the use of category theory concering the Formalization 
Thesis, I do not see what the advantage might be.  As I have previously 
written, a category is defined in terms of ZFC, as is the concept of a 
functor between two categories.  If "category" is not defined in this 
manner, I have previously asked for someone to give an explicit example 
of a statement concerning a category which can not be equivalently 
reformulated using the the notion a cateogry is a sextuble consisting of 
its objects, its morphisms and the source, target, identity and 
composition functions.

I see though a more serious problem with regard to relating the 
Formalization to "categories of translations".  Namely, do the 
"categories of translations of a fixed mathematical statement" form a 
2-category or a bicategory?  And, whatever the proposed answer to this 
question is, why stop with n-categories (whether strict or lax) for any 
fixed n, why not involve (n+1)- categories as well.  In the limit, there 
are, of course infinity-categories and why should they not enter.  Such 
objects are these days not so esoteric, and have certainly entered into 
"category theory" itself, but also into homotopy theory, initially via 
Grothendieck's 600 page manuscript Pursuing Stacks (begun as a letter to 
Quillen), but these days pursued by many others, algebraic geometry, via 
work of Simpson, Toen and others on higher stacks, ....

Like Shipman, I would like to see an explicit example of a mathematical 
statement that can not be formalized in ZFC (or possibly ZFC + 
Grothendieck's axioms on universes).

William Messing