Cyberax wrote:Basically, I suspect you have wandered off into the realm of "take a sphere, cut it up, rotate, translate, get 2 spheres", in which the truth of your theorum depends on axioms which you can flip-flop either way.

That's Banch-Tarski paradox - a result of application of axiom of choice. I'm not sure if we need it to construct our system.

It's "Banach-Tarski", by the way, in case that wasn't just a typo.

When we're talking about the existence of complete extensions of theories, we don't need the axiom of choice or any of the other axioms which you might find suspicious. Complete extensions of theories do exist, and the statements about mathematical logic that you can prove by using the existence of complete extensions of theories are true in standard ZF set theory, without the axiom of choice (i.e. provable from all of the usual axioms mathematicians use, even without using choice).

Statements which are provable

in your complete extension of a theory, however, are in general very suspicious and wishy-washy. Unless you started out with a complete theory to begin with, you are making many many choices about the axioms you use, and so you can end up with all sorts of different statements being true or false in the complete extension. But that's not what we use it for - the existence of a complete extension is generally used in such a way that we don't care what the complete extensions is, or what statements are provable from the ridiculously unknowable set of axioms we chose when constructing it. We just care that the fact that complete extensions exist is useful for proving some interesting statements about the theories we actually do work with. In other words, there are proofs that follow the basic structure:

1) Start with a theory we like, such as PA.

2) Extend PA to a complete theory T.

3) Prove some result about T by using, among other things, the fact that it is complete.

4) Show that the result you proved of T implies some interesting fact about PA.

5) Conclude that PA has some interesting previously unknown property.

Yakk, do you buy what we're doing now? Just because a proof requires a step that we can't explicitly construct doesn't mean it's result is false. At least, not unless you agree with Brouwer and think that you have to be able to construct something for it to exist, i.e. that continuous self-maps of closed unit balls may not have fixed points.

I'm looking forward to the day when the SNES emulator on my computer works by emulating the elementary particles in an actual, physical box with Nintendo stamped on the side.

"With math, all things are possible." —Rebecca Watson