[FOM] Micro Set Theory

joeshipman at aol.com joeshipman at aol.com
Wed May 15 11:23:17 EDT 2013

If the informal proof can be translated into a formal proof with a blowup that is less than fully exponential, then V_7 is enough, because we only need the formal proof to have length (2^65536)/k where k is a relatively small blowup factor to code up ZFC-proofs as integers.

ZFC is powerful and flexible enough that I doubt extremely strongly that any "informal" proof that mathematicians would accept, that is formalizable in ZFC at all, would require a fully exponential blowup. Harvey has shown that there are fairly simple propositions following from large cardinals which have ZFC proofs but only of infeasible size; however, the arguments for the TRUTH of those propositions depend on the large cardinals and are not simply informal versions of ZFC-formalizable proofs.

In other words, our informal proofs outstrip formal knowledge of V_7 only to the extent they outstrip ZFC itself.

I think V_6 is where the action is, but I'd like to know if there is anything interesting that V_5 can tell us.

-- JS

-----Original Message-----
From: meskew <meskew at math.uci.edu>
To: Foundations of Mathematics <fom at cs.nyu.edu>
Sent: Wed, May 15, 2013 10:59 am
Subject: Re: [FOM] Micro Set Theory

> If V_0 is the empty set and V_(i+1) is the power set of V_i, then the
> elements of V_7 have infeasible size and can code objects smaller than
> 2^65536, so that an oracle for the theory of V_7 would allow answers to
> any mathematical question we care about (for example "Does the Riemann
> Hypothesis have a proof from ZF + your favorite large cardinal axiom of
> length < 10^1000 ?"), thereby rendering mathematicians obsolete.

I'm not convinced. So often, informal proofs capture so many bits of
formal implementation in so few words, especially when we apply
meta-theorems about the formal system, and build on previous such work in
a way that would seem to increase the formal implementation task
exponentially. It seems plausible that our informal proofs can outstrip
the formal knowledge of V_7. What do you think?


FOM mailing list
FOM at cs.nyu.edu

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130515/cd40453a/attachment-0001.html>

More information about the FOM mailing list