Specker sequence

More generally, a Specker sequence is called a recursive counterexample to the least upper bound principle, i.e. a construction that shows that this theorem is false when restricted to computable reals.

In fact, the proof of the forward implication, i.e. that the least upper bound principle implies ACA0, is readily obtained from the textbook proof (see Simpson, 1999) of the non-computability of the supremum in the least upper bound principle.

The definition of qi causes a single binary digit to go from 0 to 1 each time i increases by 1.

Thus there will be some n where a large enough initial segment of x has already been determined by qn that no additional binary digits in that segment could ever be turned on, which leads to an estimate on the distance between qi and qj for i,j > n. If any such a function r were computable, it would lead to a decision procedure for A, as follows.

To complete the decision procedure, check these in an effective manner and then return 0 or 1 depending on whether k is found.