[FOM] Weak foundations for cohomological number theory

[Colin McLarty]

Hello,

I can now show that the Grothendieck-Deligne proof of the Weil
conjectures, and Wile's and Kisin's proofs of Fermat's Last Theorem,
can be formalized in Bounded Zermelo Fraenkel set theory with choice.
This is the finitely axiomatized fragment of ZC where the separation
axiom scheme is restricted to bounded (delta-nought) formulas, so ZC
proves it is consistent.  It has the proof-theoretic strength of
simple type theory.  Following Mathias I call it MacLane set theory.

The whole apparatus of Grothendieck's SGA can be formalized in that
set theory extended by an axiom positing one suitable universe U.
That set theory proves the universe U is an omega-model of ZC, while
the theory itself is modeled by the ZFC set V-sub-omega-times-3.

Both cases are shown by general considerations on the tools involved.
I'm sure both remain great overestimates of the proof-theoretic
strength of FLT and the Weil conjectures.  But sharp estimates will
presumably require a huge amount of new arithmetic specific to each
proof.

I am finishing up a paper on this which I will post on my website as
soon as it is presentable.  Thanks to all who have answered my
questions about this.

best, Colin