[FOM] Formalization Thesis
messing
messi001 at umn.edu
Fri Jan 4 08:52:08 EST 2008
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
More information about the FOM
mailing list