[FOM] Proving FLT in PA
avigad at cmu.edu
Wed Feb 22 08:56:25 EST 2006
Joe Shipman wrote:
> However, there are many other theorems of number theory and algenraic
> geometry proved that use the full machinery Grothendieck and others
> developed, and nobody ever gave a satisfactory answer to my repeated
> query "WHERE is the metatheorem that allows us to tell when the
> 'Universes' assumption can be eliminated?"
> I think this ought to be considered scandalous.
Solomon Feferman has written a number of papers on ways to handle
category-theoretic universes in ZFC. The latest is here:
It provides references to the others.
A strategy towards showing that FLT can be formalized in weak theories
is to proceed as in Feferman's [1969,2004], and show that (with both
real work and proof-theoretic tricks) one can get by with only mild
closure conditions on the universes. But the number theory is beyond me,
so I don't know where the sticking points may be.
More information about the FOM