[FOM] Micro Set Theory

[joeshipman at aol.com]

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?

Monroe

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom

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