FOM: Nice idea, fwd from Feferman

[Colin McLarty]

        Sol Feferman asked me to forward this. It began when I asked him
about a friend of mine who suggested Feferman had once studied "universes"
defined as V(i) for i any limit ordinal. I will only add that I believe he
is right about the minimal proof theoretic strength needed for Wiles's proof.

>'s recollection is far from the idea.  What is needed is that V(i)
>is formally treated as an elementary substructure of V.  That can be done
>by adding an additional symbol for such a universe, and adding, formula by
>formula, the axioms that it forms an elementary substructure of V (with
>the membership relation).  I did this in a paper "Set-theoretical
>foundations of category theory" in _Reports of the Midwest Category
>Seminar III, Lecture Notes in Math. vol. 106 (M. Barr, et al, eds.) 1969,
>pp. 201-247.  I considered a few theorems from general category theory and
>showed how they can be reformulated here, using "small" to mean a member
>of such a "universe".  Examples that go through are the Adjoint Functor
>Theorem and Yoneda's Lemma.  A question was raised (I think by Isbell at
>the time) about some theorems like the Kan Extension Theorem, which on the
>face of it require the ordinal of the universe to be inaccessible.  If one
>adds that assumption, the theory is conservative over ZFC plus a statement
>of existence of Mahlo cardinals of the first kind (very low large
>cardinals in today's pantheon of large cardinals).  
>  I gather this has been a matter for discussion recently on the fom list.
>Would you please communicate the above information to the interested
>parties there.  
>
>Thanks,
>Sol Feferman
>
>PS. I also indicated in my article that usual homological algebra, as e.g.
>in MacLane's Homology book, can be formalized in the theory I
>described, with a "universe" symbol for the "small" sets, conservative 
>over ZFC.
>
>  I would be extremely skeptical as regards the possible necessity of
>universes in Wiles' proof.  Indeed, it has been speculated that the proof
>can be formalized in a system conservative over Peano Arithmetic.  I don't
>know what, if any, evidence for this there is.  But it would be doubtful
>if his proof really needed much of impredicative set theory.  Only a
>detailed analysis would settle this, though.  That has nothing to do with
>what mathematicians feel is conceptually necessary to understand his
>proof.

>Dear Colin,
>  The V(i) with i a limit ordinal (take it to be greater than omega in
>order to satisfy the axiom of infinity), do not in general satisfy the
>replacement axiom.  That is one reason more is done.  Another reason is
>that by making the set s = V(i) an elementary substructure of V and
>reading "small set" to mean--element of s--any result about small sets,
>small categories, etc. can be transferred to V, so that it becomes a
>result about sets, resp. categories in general.  That is one way to show
>that the distinction between small and large categories or between
>categories in one universe and those in another universe, is not an
>essential distinction, though something like it seems to be needed for the
>current set-theoretical foundations of category theory.  The use of the
>'s' theory I described aims to have it both ways, to have your cake and
>eat it too.
>  Please pass on this clarification with your fom communications.
>
>Best,
>Sol