FOM: Challenge axioms, final draft

[Till Mossakowski]

Kanovei wrote:
> 
> For instance the SET declaration would be that
> --------
> set theory adequately presents all legitimate
> mathematical objects as sets, supports all known
> correct ways of mathematical reasoning, and
> converts all known mathematical theorems to
> theorems about sets (or: theorems of ZFC).
> ---------

I want just note that category theory (which certainly
is a part of mathematics) often needs stronger foundations.
A considerable part of category theory is about "smallness
properties", i.e. the question whether a collection is
a set or only a class. For this, you need ZFCU (where
U states the existence of a set-theoretic universe)
as foundation. Of course, you can turn each theorem T
of category into a theorem of ZFC by writing

	ZFC |- U => T

instead of

	ZFCU |- T

(and indeed, there may people having doubts adding U
to foundations because ZFCU is more likely to be inconsistent
than ZFC).

But then why not also write

	ZF |- (AC /\ U) => T

- there seems to be a discussion at the fom list about the status of AC,
so is it entirely clear that it belongs to foundations?
After all, there is a large number of theorems of form

	ZF |- AC <=> X

where X is some well-known theorem of set theory or topology
(say, a product of compact Hausdorff spaces is compact).
Thus probably, most times we use ZFC as foundations, but for
these studies, we only use ZF.

Now one further generalization would be to write

	ToposTheory |- ("ZFC" /\ Trans(U)) => Trans(T)

where "ZFC" is some (conjunction of) axioms stating that
our topos is indeed a model of ZFC, and Trans is the translation
of ZF-formulae to topos theory.
Again, most times we use ZFC as foundation, but some
times, we want to be more general and use topos theory.

Now what is the problem here? The translation function Trans?
The extra generality of topos theory?

Greetings,
Till Mossakowski