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][1], 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.


  [1]: http://en.wikipedia.org/wiki/Specker_sequence