FOM: The logical, the set-theoretical, and the mathematical
kanovei at wmwap1.math.uni-wuppertal.de
Tue Sep 12 15:34:57 EDT 2000
>The Axiom of Choice has a special status. It is not necessary for the
>development of number theory, but is certainly an essential part of
>ordinary mathematical practice for analysis
If one commits to consider only Borel objects then all
usual instances of Choice necessarily e.g. to prove that
a ctble union of null sets is null, become provable in ZF
without choice. Yet I don't know if anybody has developed
this observation into a careful theory.
>Harvey's insistence that ZFC captures the intuition about sets that
>mathematicians had all along (presumably from Cantor c. 1880 to 1930)
>seems ahistorical. There were several unsuccessful or incomplete
>attempts to formalize sets and classes, and Type Theory must still have
>been considered an important alternative (to set theory) foundation of
Type Theory is not an alternative but rather a veaker version
because it follows generally the same cumulative construction
of objects, but voluntarily restricted to the first w steps.
As a foundational system, TT is in a minor league
because what it suffices to foundate, like analysis, is self-foundated
in a sense, by Dedekind etc.,
anyway TT misses set theory, topology, perhaps some branches of
algebra, so it cannot count as "foundation of [all of] mathematics".
Even in descriptive set theory (essentially 2nd order PA), normally
within the reach of TT, there are absolutely mathematically meaningful
(ie, not something like "I am not provable")
and well defined sentences provable in ZFC but not in TT (and ZC).
NF is perhaps the only known alternative to ZFC as foundations,
but it so drastically contradicts practice of mathematical
reasoning that almost everything simple in ZFC (and "naive" mathematics)
needs tricky reasoning in NF.
More information about the FOM