# Is axiom of choice applicationless?

1. Sep 8, 2008

### jostpuur

Does there exist a theorem, whose proof relies on the axiom of choice, and which has practical or concrete applications? I'll consider for example PDE and number theory problems practical or concrete, because they can be intuitively connected with the physical world. On the other hand, for example non-measurable sets hardly have effect on anything, except on abstract theory.

2. Sep 8, 2008

### Count Iblis

Well, everything we can observe is formally describable, at least we don't have any evidence to the contrary. So, although we can talk about the set of real numbers being a continuum (most of which are not formally describable as Turing showed) and then needing to postulate the Axiom of Choice to "legalize" the act of choosing an element from such a set, even though there is no formal describable way to do that, this doesn not prove that we really need this.

This is similar to postulating a God and then finding out that it is a hypothesis we don't really need, although it can be useful in practice (e.g. to get elected as President).

In first order logic, you only need countable sets, http://www.earlham.edu/~peters/courses/logsys/low-skol.htm" [Broken]. This means that any model which is uncountable can be reinterpreted as a countable model.

Last edited by a moderator: May 3, 2017
3. Jan 5, 2009

### Hurkyl

Staff Emeritus
The theorem that every field has an algebraic closure depends on the axiom of choice. I believe the proof that it is unique also needs AoC. I would imagine that lots of the theory involving them (e.g. Galois theory) would need AoC to function properly.

Algebraic closed fields are important for algebraic geometry and algebraic number theory; I've once heard something to the effect that most of modern algebraic number theory is concerned with the study of the Galois group $\mathrm{Gal}(\bar{\mathbb{Q}} / \mathbb{Q})$.

While I suspect you might be able to construct $\bar{\mathbb{Q}}$ without AoC, I wouldn't dare make any predictions about how infinite Galois theory would behave. And even if you can... you still need algebraic closures of finite fields, which you don't get without AoC.

Maybe the theorems you want can be proven without algebraically closed fields -- but they'll be much more difficult to show. Maybe the calculations you want to do can be done without algebraically closed fields -- but the theorems that say how to go about doing it might still rely on them.

As for PDE's, Hilbert spaces, and so forth -- I wouldn't dare make any claims as to what would even still work in those theories if you cast out the AoC! I would be too afraid of missing an assumption that depends on some vector space having a basis, or some functional existing, or some set being closed, or such and such that simply isn't true without the AoC.

4. Jan 5, 2009

### Hurkyl

Staff Emeritus
I suspect you've fallen into a trap -- confusing the internal theory with the external theory. (e.g. see Skolem's paradox) Within your (externally) countable model of first-order set theory, you still have (internally) uncountable sets -- e.g. you still have the theorem that $|\mathbb{N}| < |\mathbb{R}|$. There simply does not exist an internal bijection of the (internal) sets N with R, despite the fact that there does exist an external bijection.

Last edited by a moderator: May 3, 2017
5. Jan 5, 2009

### HallsofIvy

Staff Emeritus
The proof that any (infinite dimensional) vector space, such as Hilbert Space, has a basis uses Zorn's lemma which is equivalent to axiom of choice.

6. Jan 6, 2009

### jostpuur

I don't much about Galois theory, so I cannot say anything about it.

About PDEs and Hilbert spaces... for example the Fourier modes in $L^2([0,2\pi],\mathbb{C})$ exist fine without AOC. I see that the study of PDEs naturally leads to the study of infinite dimensional vector spaces, and on the other hand the study of infinite dimensional vector spaces naturally leads to the AOC. So one might think that PDEs naturally lead to AOC, but I disagree on this. If you actually fix some concrete vector space, the useful basis usually exist without AOC. I bet you cannot point out an example of a PDE, whose solution's existence depends on AOC.

7. Jan 6, 2009

### maze

I suspect that Zorn's lemma is required to find the basis for a general Sobolev space.

If this is true, you could look for examples of Sobolev spaces that require Zorn's lemma for a basis, and then invent a PDE using that space.

8. Jan 6, 2009

### gel

I don't think you need the axiom of choice for anything, except to make things easier. Trying to do a lot of maths without at least dependent choice (which is a countable version of AOC) would be very tedious.

Also, you could take any proof using AOC and rewrite it to prove that "if such and such a choice function exists then ...". in any applications you would hopefully be able to find the necessary choice functions and then apply the theorem without AOC. If you can't, then I'm not sure that your theorem is really that helpful (i.e. you've proved something exists but have no way of constructing it).

Maybe HallsofIvy's post illustrates my point.

without AOC you could say that.
if a Hilbert space H has a choice function mapping any closed proper subspaces to an element of H not in that subspace, then H has an orthonormal basis.

In fact the choice function picks out a unique such basis. In many cases you can describe such a choice function too.
If you can find a sequence of elements x_1,x_2,x_3,... whose linear span is dense in H then there is a choice function taking a subspace V to the first x_k not in H.

Last edited: Jan 6, 2009
9. Jan 6, 2009

### Hurkyl

Staff Emeritus
I would like to point out that, oddly enough, if you're really serious about constructivism, then it turns out that the axiom of choice is actually a theorem. (at least as I understand things) Of course, you have to be careful about all of the other things that become more complicated....

10. Jan 6, 2009

### gel

well, $\bar{\mathbb{Q}}$ is just the set of algebraic numbers in the complex number field, which constructs it. You don't need AOC for algebraic closures of finite fields either.
You do need it for the infinite galois group $\operatorname{Gal}(\bar{\mathbb{Q}}/\mathbb{Q})$ though. I think you could still do algebraic number theory without it, but you'd have to replace the elements of the galois group with elements on finite but arbitrarily large extensions of Q. AOC makes life easier but leads to very nonconstructive proofs.

11. Jan 6, 2009

### Marcaias

From Wikipedia:

12. Jan 6, 2009

### Hurkyl

Staff Emeritus
Oh bleh, and I just went through all this a couple years ago too. Woe is me and my spotty memory! What about the p-adic fields? I imagine you can do those too, then.

13. Jan 6, 2009

### Marcaias

Whoa, a theorem in what? Gödel showed it is not a theorem in ZF, and neither is its negation (assuming ZF is consistent, of course.)

14. Jan 6, 2009

### gel

aah yes. I remember hearing something like that too. I'm a bit vague about it, but I expect that it is a theorem in the "metalanguage", and not inside the logic itself. That is, constructivism restricts what you can construct so much that there's not really any arbitrary choices left to be made.

15. Jan 6, 2009

### gel

Hmm, not sure, I'd have to think about it...

...

no, you don't need AOC!

you only need to add roots of integer or rational polynomials, because they're dense, and they can be well ordered - which should avoid AOC.

(that's my first thought. haven't been through the details)

Last edited: Jan 6, 2009
16. Jan 6, 2009

### CRGreathouse

The constructive axiom "V = C" implies AC in ZF.

17. Jan 6, 2009

### Hurkyl

Staff Emeritus
I confess that I don't know how constructivist set theory is done from a formal logic viewpoint. But I can state a version of choice for Turing macines; I strongly suspect the analogous theorem for constructivist set theory is similar in spirit (if not actually the same).

Theorem: There exists a Turing machine AC that has the following behavior on a string M.
1. If M is a description of a Turing machine T that accepts at least one string, then AC accepts M, and outputs a string AC(M) that is accepted by T
2. If M is a description of a Turing machine T that never accepts anything, then AC doesn't halt
3. If M is not a description of a Turing machine, then AC rejects M.

If we interpret a Turing machine T as being analogous to a set (i.e. $x \in T$ is defined to mean "T accepts x"), then AC computes an explicit choice function on the class of all nonempty sets.

One implementation of AC is as follows:
Code (Text):

If M is not a turing machine description, Reject.
For every pair of natural numbers m, n:
Let S be the n-th string
Simulate M for m steps on S
If M has accepted S, then Accept and output S

(where I've assumed we've chosen an enumeration of all strings, and an enumeration of all pairs of natural numbers)

Last edited: Jan 6, 2009
18. Jan 6, 2009

### gel

but strings are well ordered, so AOC for subsets of such things is trivial anyway. Is that really enough to imply AOC for constructive logic

(AOC applies to sets of nonempty sets. Maybe any constructive proof that the sets are nonempty can be converted to a choice function. Seems reasonable, but I'm not very familar with constructive logic.)

Last edited: Jan 6, 2009
19. Jan 6, 2009

### Hurkyl

Staff Emeritus
My understanding of constructivist set theory (and related things) is that it's very closely related to computability theory, so I suspect that it is enough.

However, my quote that AoC is a theorem is relayed by a friend of mine who studied non-standard analysis (NSA): he loves to tell the story about how he'd explain his discipline to most mathematicians, and they'd view it with suspicion because of the way it uses AoC... so when he was explaining it to a constructivist, he expected to be outright rejected, and was completely taken aback when the constructivist had absolutely no problems with NSA's foundations, because AoC becomes the "theorem of choice".

20. Jan 6, 2009

### Marcaias

Ahh, thank you.