FOM: Functors and Diophantus, reply to Kanovei

[Colin Mclarty]

kanovei at wminf2.math.uni-wuppertal.de wrote:
        
>    Is there any known statement A such that 
>   
>    1) A is a meaningful mathematical statement 
>       (e.g., NOT of the form Con ZFC)
>    2) A is formalizable in set theoretic language 
>       (e.g. NOT on existence of some "universe")
>    3) A is NOT provable in ZFC 
>    4) A is provable in ZFC + "universes" or "topoi" or the like. 

Requirement 2 is incoherent since Grothendieck universes 
themselves are formalized in set theoretic language. They are
not a new primitive.
      
My post yesterday on alternatives to ZFC referred to several
volumes of statements meeting requirements 1, 3, and 4, by 
Grothendieck, Deligne. et al, and a graduate textbook by Tamme. 
Here I will give an example from Cornell, Silverman, and 
Stevens editors, MODULAR FORMS AND FERMAT'S LAST THEOREM 
(Springer 1997) reporting the 1995 Boston University 
meeting on Wiles's proof.
    
As motivation Barry Mazur tells us "Hendrick Lenstra in his lecture
at the conference recounted that twenty years ago he was firm in
his conviction that he DID want to solve Diophantine equations and
he DID NOT wish to represent functors--and now he is amused to
discover himself representing functors in order to solve Diophantine
equations!" (Cornell et al. p.245). 
    
Mazur and Lenstra refer to methods using theorems such as this:
"For any scheme S, the category Sch/S of schemes over S has binary
products". Or, to give a quote:
    
"(For any ring R) the category of affine R-group algebras is 
anti-equivalent to the category of commutative Hopf algebras
over R" (John Tate, in Cornell et al. p.126).
    
    
These theorems speak of sets whose existence is not provable 
in ZFC but is trivially provable assuming Grothendieck 
universes. They quantify over such sets.
    
Understand: No one in the world believes that this kind of
math requires anything like the proof theoretic strength of
ZFC plus Grothendieck universes. Zermelo set theory with 
choice, or something like that, ought to be STRONG enough. 
But it is not "roomy" enough. The only foundations known to 
date which allow these clear simple theorems, use some 
variant of Grothendieck universes. The only alternative
to universes in widespread practical use is to ignore the
foundational problems and act as if proper classes are sets.         
        
The theorems as stated are universally believed by the experts,
and used in the literature, and not provable in ZFC without
universes.