[FOM] Proving FLT in PA

[Jeremy Avigad]

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:

   http://math.stanford.edu/~feferman/papers/ess.pdf

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.

Jeremy Avigad