FOM: The logical, the set-theoretical, and the mathematical

[Kanovei]

>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
>mathematics 

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. 

Vladimir Kanovei