# Axiom of choice and convergence

Hi fellows,

I was wondering. Is the axiom of choice used to show that $\mathbb{R}$ is complete? If yes, is there a way to construct monotonic bounded sequences that do not converge?

-
No, you don’t need the axiom of choice for that (unless you employ a weird definition of $\mathbb R$ or of completeness). – Emil Jeřábek Feb 1 '12 at 10:35
The meta-reason is: Limits are unique. – Martin Brandenburg Feb 1 '12 at 12:20
Jean-Luc, I would think that this question fits better on math.SE. – Asaf Karagila Feb 1 '12 at 12:41

The standard construction(s) of $\mathbb R$ do not use the Axiom of Choice. Therefore one cannot construct a bounded monotone sequence that does not converge.

Maybe, it worths to say that there are also constructions of $\mathbb R$ that makes use of AC. See for instance http://en.wikipedia.org/wiki/Construction_of_the_real_numbers, where it is proposed the following construction: take the ring of bounded hyperrationals and quotient out the maximal ideal of infinitesimals. One gets the real numbers. Here, AC is used in actually the weaker form of the ultrafilter lemma (existence of free ultrafilters).

-
I guess that's it. But I can remember reading a couple of month ago some kind of non convergent sequence on the real line. Could it be that constructivsm reject something at one point, and therefore manage to exhibit such a sequence? – Jean-Luc Bouchot Feb 1 '12 at 11:13
Constructivism rejects the law of excluded middle. And indeed, it is not constructively provable that every bounded monotone sequence has a limit. This is closely connected to the fact that there are computable monotone sequences whose limit is not computable. – Emil Jeřábek Feb 1 '12 at 11:25
I should stress that the reals are constructively complete, in the sense that every Cauchy sequence converges. The nonconstructive part in the monotone convergences theorem is to show that a bounded monotone sequence is Cauchy. – Emil Jeřábek Feb 1 '12 at 11:46
Perfect! Thanks a lot. Do you have any pointers to those things? – Jean-Luc Bouchot Feb 1 '12 at 11:55
Found what I was looking for! (my question was a bit far away, I have to admit!): en.wikipedia.org/wiki/Specker_sequence – Jean-Luc Bouchot Feb 1 '12 at 12:11

In constructive mathematics we do not need the axiom of choice to show that the (two-sided) Dedekind cuts form an ordered archimedean field which is complete in the sense that every Cauchy sequence converges.

However, it is possible to define a monotone bounded sequence, known as a Specker sequence, such that it is not provable constructively that the sequence has a limit.

We may ask what is needed to prove that every monotone bounded sequence has a limit. It is sufficient to assume the principle LPO, which states that every binary sequence is either constantly 0 or it contains a 1. In fact, if every monotone bounded sequence has a limit, then LPO holds. Again (as far as I can see), no choice is involved.

-