I am surprised that the following theorem requires axiom of choice:
Theorem: For any real number x, there is a sequence x̂ : ℕ → ℚ converging to x.
It seems to me that it has a constructive proof with computable x̂, it goes like this:
To calculate x̂(n):
Start with a = 1, repeat a = a * 2 while |x| > a. This will end in a finite number of steps.
Start with the segment [-a, a]. On each step split it in half and pick the half that contains x (if x is exactly in the middle, pick the left half). Repeat this exactly n times. The last splitting point is x̂(n).
Here we have an algorithm that calculates x̂(n) in a finite number of steps for any particular x and n, so x̂ is computable.
Do note the followup that axiom of countable choice is constructively computable and therefore the choice-using proof goes through computably. The universe that kills countable choice is not the computable universe RT(K1), but rather the continuous universe Sh(ℝ), where everything is a continuous function out of the real numbers. The failure of “For any real number x, there is a sequence x̂ : ℕ → ℚ converging to x.” in that universe translates to the failure of “For any continuous function x : ℝ → ℝ, there exists a continuous family of sequences x̂ : ℝ×ℕ → ℚ converging to x.”. The trouble with that statement is that ℚ is discrete, so x̂ is forced to be constant in its first parameter.
Your proof is perfectly valid in classical math with excluded middle. However, classical math lacks the computational substance that this post centers around.
Start with a = 1, repeat a = a * 2 while |x| > a. This will end in a finite number of steps.
“While |x| > a” requires excluded middle over |x| > a. Constructively, the inequality operator for real numbers only supports a weaker form of excluded middle called comparison: if x < y then x < z or z < y. Not a huge problem for this part of the proof as you could just case split by |x| > a or |x| < a+1.
Though if you do this, because these are overlapping conditions, its no longer deterministic, so a isn’t a function of x.
You essentially just want a rational upper bound for x, though. This does exist (not as a function as that would be discontinuous) and you don’t need to do an algorithm for figuring it out. (Under the hood in RT(K1), this is essentially because representations of real numbers come packaged with an upper and lower rational bound.)
Start with the segment [-a, a]. On each step split it in half and pick the half that contains x (if x is exactly in the middle, pick the left half). Repeat this exactly n times. The last splitting point is x̂(n).
“Pick the half that contains x” requires excluded middle too, for comparing the midpoint with x. Again you could probably add an epsilon of leeway to let comparison go through, but then there’s no functional relationship, and you need countable choice to pin down x̂.
I am surprised that the following theorem requires axiom of choice:
It seems to me that it has a constructive proof with computable x̂, it goes like this:
To calculate x̂(n):
Start with a = 1, repeat a = a * 2 while |x| > a. This will end in a finite number of steps.
Start with the segment [-a, a]. On each step split it in half and pick the half that contains x (if x is exactly in the middle, pick the left half). Repeat this exactly n times. The last splitting point is x̂(n).
Here we have an algorithm that calculates x̂(n) in a finite number of steps for any particular x and n, so x̂ is computable.
Do note the followup that axiom of countable choice is constructively computable and therefore the choice-using proof goes through computably. The universe that kills countable choice is not the computable universe RT(K1), but rather the continuous universe Sh(ℝ), where everything is a continuous function out of the real numbers. The failure of “For any real number x, there is a sequence x̂ : ℕ → ℚ converging to x.” in that universe translates to the failure of “For any continuous function x : ℝ → ℝ, there exists a continuous family of sequences x̂ : ℝ×ℕ → ℚ converging to x.”. The trouble with that statement is that ℚ is discrete, so x̂ is forced to be constant in its first parameter.
Your proof is perfectly valid in classical math with excluded middle. However, classical math lacks the computational substance that this post centers around.
“While |x| > a” requires excluded middle over |x| > a. Constructively, the inequality operator for real numbers only supports a weaker form of excluded middle called comparison: if x < y then x < z or z < y. Not a huge problem for this part of the proof as you could just case split by |x| > a or |x| < a+1.
Though if you do this, because these are overlapping conditions, its no longer deterministic, so a isn’t a function of x.
You essentially just want a rational upper bound for x, though. This does exist (not as a function as that would be discontinuous) and you don’t need to do an algorithm for figuring it out. (Under the hood in RT(K1), this is essentially because representations of real numbers come packaged with an upper and lower rational bound.)
“Pick the half that contains x” requires excluded middle too, for comparing the midpoint with x. Again you could probably add an epsilon of leeway to let comparison go through, but then there’s no functional relationship, and you need countable choice to pin down x̂.