[FOM] Micro Set Theory

[meskew at math.uci.edu]

> 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