Constructivist mathematics does not depend on the axiom of choice.
That said, when you only admit a universe of mathematical objects that admit of a finite construction, it is not unreasonable that you can have a computer program that, at least in principle, will enumerate all possible constructions and proofs of statements about them. Given that, you can create a construction which is literally for each set Y, the primary x in Y is the first x which in that enumeration a statement of the form "x is in Y" is proved.
This construction give a choice function of the kind that the Axiom of Choice says exists. However that said, the bizarre consequences of the Axiom of Choice that you find in classical set theory can't be proven for other reasons.
Thank you for the clarification. Following up on this, I found a blog post [0] that explains why you don't get bizarre consequences like the Banach-Tarski paradox this way:
> [The constructivist method] avoids the basic problem with the axiomatic problem. You can’t have something ridiculous like the set of all sets that don’t include themselves, because the only way to show that a set exists is to show a process to create it – and there’s no way to create a paradoxical set! You don’t get nonsense like [the Banach-Tarski paradox], because the division of the spherical topological space into the non-metric subspaces is impossible: you can’t show a process that produces it. In the world of intuitionism and constructivism, existence proofs that don’t produce concrete examples don’t exist!
That said, when you only admit a universe of mathematical objects that admit of a finite construction, it is not unreasonable that you can have a computer program that, at least in principle, will enumerate all possible constructions and proofs of statements about them. Given that, you can create a construction which is literally for each set Y, the primary x in Y is the first x which in that enumeration a statement of the form "x is in Y" is proved.
This construction give a choice function of the kind that the Axiom of Choice says exists. However that said, the bizarre consequences of the Axiom of Choice that you find in classical set theory can't be proven for other reasons.