Is axiom of choice applicationless?

[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.

 

[Count Iblis]

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.

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" . This means that any model which is uncountable can be reinterpreted as a countable model.

LST has bite because we believe that there are uncountably many real numbers (more than \aleph_0). Indeed, let's insist that we know it; Cantor proved it in 1873, and we don't want to open the question again. What is remarkable about LST is the assertion that even if the intended interpretation of S is a system of arithmetic about the real numbers, and even if the system is consistent and has a model that makes its theorems true, its theorems (under a different interpretation) will be true for a domain too small to contain all the real numbers. Systems about uncountable infinities can be given a model whose domain is only countable. Systems about the reals can be interpreted as if they were about some set of objects no more numerous than the natural numbers. It is as if a syntactical version of "One-Thousand and One Arabian Nights" could be interpreted as "One Night in Centerville".

 

[Hurkyl]

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.

 

[Hurkyl]

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

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.

 

[HallsofIvy]

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.

 

[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.

 

[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.

 

[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.

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.

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.

 

[Hurkyl]

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...

 

[gel]

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.

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.

 

[Marcaias]

From Wikipedia:

The proof of the independence result also shows that a wide class of mathematical statements, including all statements that can be phrased in the language of Peano arithmetic, are provable in ZF if and only if they are provable in ZFC. Statements in this class include the statement that P = NP, the Riemann hypothesis, and many other unsolved mathematical problems.

 

[Hurkyl]

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.

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.

 

[Marcaias]

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...

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.)

 

[gel]

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.

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.

 

[gel]

What about the p-adic fields? I imagine you can do those too, then.

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)

 

[CRGreathouse]

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.)

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

 

[Hurkyl]

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:

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)

 

[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.)

 

[Hurkyl]

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?

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".

 

[Marcaias]

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

Ahh, thank you.

 

[Hurkyl]

p.s. I should point out that constructivism is different than just using intuitionistic logic. In fact, when doing intuitionistic set theory, the the axiom of choice implies your logic is actually classical.

 

[gel]

say two real numbers are equivalent, x~y, if x-y is rational. Let S be the set of equivalence classes. They are nonempty by definition. Then choose one element from each to get a set A. A isn't measurable.

Where does that go wrong with constructive logic.

 

[Hurkyl]

My recollection of constructive analysis is that real numbers are defined (by one definition) by computable Cauchy sequences of rational numbers. In particular, the relation "x is rational" wouldn't be a computable relation on the reals.

(I'm not having any luck finding a good online source for constructive analysis. Bleh)

 

[gel]

but given any subset S of the reals, if S != 0 and S !=R then it must have a boundary point, and if a cauchy sequence converges to such a point you can't tell if it is in S or not.
So, in constructive logic, the only subsets of the reals are emptyset and R. Is that true?
Seems to follow from what you said, but I don't know what you're allowed to do in CL

 

[Hurkyl]

(Again, I'm going to talk in terms of computability, because that's where my familiarity lies) Don't forget there are three truth values here: "accept", "reject", and "no answer". I would be willing to believe that the only decidable subsets (ones that give you a definite "accept" or "reject") of R would be the empty set and R itself, but you can have lots of other subsets whose membership relation occasionally yields "no answer".

 

[Hurkyl]

Hrm, let me amend that... with the Cauchy sequence definition, I think you're almost right. There are exactly three subsets of R:
1. The empty set (everything is rejected)
2. R (everything is accepted)
3. The set whose membership relation is always "no answer".


However, other definitions for real numbers (e.g. nested sequence of intervals whose endpoints are rational and whose length goes to zero) would allow more interesting subsets of R.

 

[jostpuur]

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.

When a Sobolev space is used to prove an existence of a solution to some PDE, isn't it the completeness of that Sobolev space that is essential, and not any particular basis?

(I don't know much of Sobolev spaces, but some lecture notes of one other course mentioned something about them in the beginning, so I have some idea.)

 

[Diffy]

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.

Even if there was such a theorem, what makes you think you can chose it?