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, suffices. In fact, if every monotone bounded sequence has a limit, then LPO holds. Again (as far as I can see), no choice is involved.

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.