[jaydaigle]

ketralnis is right that this only terminates if an algorithm exists, so the claim that this terminates is equivalent to the axiom of choice.

But I'd also add that you can have a choice function that isn't an "algorithm". An algorithm, at least in the sense I'd generally interpret the word, has finitely many instructions and at most countably many steps. If we have uncountably infinitely many uncountably infinite sets, it is possible to have a choice function that can't be described in a finite algorithm.

Like, think about a well-ordering of the reals. If you believe the axiom of choice, then one exists. But you can't tell me what it is, because that would involve handing me infinite amounts of information. And similarly you can't write down an algorithm to produce it, without writing down infinite amounts of data.

[shadowlight]

> ketralnis is right that this only terminates if an algorithm exists, so the claim that this terminates is equivalent to the axiom of choice.

No my algorithm above will never terminate. There's a recursive call where the input never shrinks and it won't converge on a base case.

It's equivalent to saying

   def f(x):
       return f(x)

which is a pointless (but true) statement. The whole thing is distracting everyone.

Basically ketralnis is clarifying context which is sort of lost with my post. There's an axiom and do you believe in the axiom of not?

If the axiom can be proven then it is not an axiom. But a theorem. What I'm doing here is kind of pointless because we know it's an axiom by definition, the question is whether this axiom is valid or not. Attempting to prove the axiom is a a signal that I'm lacking clarity with the logic here.