[FOM] Weak foundations for cohomological number theory

[Robert Solovay]

Colin,

Mathias used "MacLane set theory" to refer to the theory you consider
(which he dubs ZBQC)  + "Every set is a member of a transitive set".

MacLane set theory is strictly stronger (proves more theorems)  than
ZBQC though they have the same proof-theoretic strength (are provably
equiconsistent in the metatheory PA).

By the way, I am not sure if you include foundation in your theory.
Mathias definitely includes it in ZBQC.

--Bob Solovay

On Mon, Jan 3, 2011 at 8:04 AM, Colin McLarty <colin.mclarty at case.edu> wrote:
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>