[FOM] Formalization Thesis

[Freek Wiedijk]

Joe:

>I repeat my earlier challenge: can anyone who disputes
>Chow's Formalization Thesis respond with a SPECIFIC
>MATHEMATICAL STATEMENT which they are willing to claim is
>not, despite its expressiblity in English text on the FOM
>discussion forum, "faithfully representable" or "adequately
>expressible" as a sentence in the formal system ZFC?

As someone who is very much interested in practical
formalization, I always wonder how to fit category theory
in a system with a ZFC-like foundation.

It certainly is possible to develop category theory in
ZFC, but in that case one generally only talks about "small
categories".  However, in mathematical practice one routinely
applies categorical reasoning to _large_ categories, like
the category of all sets, of all groups, etc.  That suggests
that in _that_ kind of category theory one really quantifies
over a domain that is outside set theory.

The way that this puzzle is solved in type theory is
equivalent to having all "ordinary" mathematics in the
equivalent of a Tarski universe, and then to only have the
category theory outside of this universe.

Now in the set theory of Mizar (where one has arbitrarily
large Tarski universes) that certainly is a possibility too,
but it does not feel attractive to me.  And certainly the
treatment of all groups in the Mizar library MML is _not_
restricted to a Tarski universe.  So any category theory
that is developed would not apply to anything having to do
with _that_ notion of group.

Is there a better approach that I am missing that allows
me to both have set theory as the foundation for my
formalizations, and still have me being able to develop
category theory in a way that I can apply it to the actually
interesting categories like the category of all sets,
of all groups, etc.?

I realize that this topic might already have been discussed
to death here.  In that case I'd appreciate pointers to
that discussion.

Freek