I think this should have been discussed on MO, but I don't see such a thread, so excuse me (and delete this question) in this case.
This is inspired by this discussion. I see that the tradition of arguing about the validity of the application of the axiom of choice has not died even now, and this surprises me greatly, because I never understood the meaning of these disputes.
I remember that when I was a student, once in front of my eyes, mathematicians were arguing about the "constructiveness" of some statements in Functional Analysis. The fact that the proofs use the axiom of choice was cosidered as the evidence of "non-constructiveness" of these results. And very quickly it became clear that the participants in the dispute simply do not understand that the analysis known to them at the most elementary level essentially relies on the axiom of choice (at least countable), because without it the simplest theorems, such as Bolzano-Weierstrass or the equivalence of the definitions of the limit by Cauchy and by Heine, etc. cannot be proved.
From what I have read about this, I have the impression that there are no meaningful statements in Analysis at all that do not use the axiom of choice.
That is why I want to ask people
what remains of analysis if it is built consistently without the axoim of choice, for example, in ZF (not in ZFC)?
And in general I would like to know
what remains of mathematics as a whole if it is built in ZF?
I guess that some elementary facts can be preserved in algebra, but, for example, in topology, I would be very surprised if something intelligible was preserved. Even in set theory, as far as I know, the picture sharply turns into a dense forest.
Where is all this written? I remember Boris Kushner's book on "Constructive mathematical analysis", but it's about something else, about a variant of intuitionistic mathematics, where "constructiveness", as the adepts understand it, is woven into the system of axioms of logic, not set theory. Is there any overview or a book explaining what is preserved in mathematics when it is built in ZF?
Also I would be grateful if somebody could clarify to me what I asked on a comment to the discussion that I mentioned from the beginning:
When a person asks whether the statement X is true without the axiom of choice, does he mean to remove the axiom of choice from the whole theory in which he formulates this statement, or only from the proof of X?
As I told there, in my understanding, in both cases the question becomes senseless. If the idea is to remove axiom of choice from everywhere, then there must be books on Algebra, Topology, Analysis "without axiom of choice". Where are those books? And what is the reason to discuss the possibility to remove AC from X, if you don't mean to insert X into a "Big theory withut AC"? On the other hand, if the idea is to remove axiom of choice only from the proof of the statement X, then how can this be interesting, if any proof of X that you suggest in "non-constructive theory" inevitably uses supplementary results and constructions (theorems, lemmas, definitions) which are based on AC?