[ketralnis]

The assertion that at least one selection algorithm succeeds without presenting that algorithm _is_ the axiom of choice.

By _assuming_ that program terminates, you are yourself taking the axiom of choice.

If it _does_ terminate, then it's not an axiom anymore it's a proof.

[shadowlight]

Yeah, this clarifies the logic. So because the algo above doesn't terminate it is not a proof.

The axiom of choice is an assumption that is neither known to be true or false.