[FOM] Micro Set Theory

[Andrej Bauer]

I would say that size is not the only thing that matters, the structure is
important too.

It is important that a formalization respects, or at least does not
mutilate, the inherent structure of the thing you're formalizing. For
example, it may be cool to represent lists of numbers as a product of
powers of prime numbers, but that sort of thing is going to be thoroughly
useless in practice. In practice, the formal language must allow direct and
abstract expression of the concepts involved.

Which is why the 2^65536 elements of V_7 will be of little help when you
try to encode a list of 9 elements.

Suppose that we lived in a world of fantasy where someone gave us an oracle
for V_7. We would devise (unnatural) encoding schemes for asking the oracle
all sorts of questions, and it would give us answers. Soon there would be
just one question we cared about: how does it work? We would take it apart
and study its inner mechanism to learn --- about the structure of V_7!
Because, to understand how such a magnificent piece of machinery could
answer everything there is to know about V_7, it to understand the
structure of V_7. Not the size.

With kind regards,

Andrej

On Tue, May 14, 2013 at 3:53 PM, Joe Shipman <JoeShipman at aol.com> wrote:

> 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.
>
> V_4 is trivially uninteresting; it has only 16 elements so brute force
> programming will let us answer any question about it involving up to 10 or
> so quantifiers.
>
> An oracle for V_6 would be very helpful since it would (I think but need
> to verify) let us solve instances of PSPACE-complete problems of length in
> the thousands of bits, for example calculating Ramsey numbers, but would it
> make mathematicians almost as obsolete as an oracle for V_7 would?
>
> Would an oracle for V5 tell us anything interesting at all?
>
> -- JS
>
> Sent from my iPhone
> _______________________________________________
> 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/20130516/cc535bb4/attachment.html>