What can be preserved in mathematics if all constructions are carried out in ZF? This is inspired by this discussion. I see that the debates about the necessity of the axiom of choice in this or that statement are still ongoing. In this regard, I became interested in whether there are textbooks that describe what mathematical disciplines turn into when the axiom of choice is consistently excluded from them.
It seems to me that, theoretically, nothing prevents a logician from writing a book that describes algebra or topology or analysis in some axiomatic set theory without the axiom of choice, for example, in ZF.
So my question is

are there texts describing what remains of analysis (or algebra, or topology) if it is built consistently without the axoim of choice, for example, in ZF (not in ZFC)?

I think such a text would be very helpful, because in my observation, people who argue about the application of the axiom of choice tend to focus on particulars without seeing the big picture, and moreover, having a rather vague idea of the subject.
For example, I have met analysts who believe that in analysis the axiom of choice appears only in a few statements, such as the Hahn-Banach theorem, and if you do not use them, you can consider your conscience "unstained by its application".
People on this thread have already explained to me that some things in analysis can be preserved, in particular (forgive my ignorance), it was a surprise to me that the theory of real numbers is preserved in some form (although, as far as I understand, the classical theorems of mathematical analysis mostly disappear). And apparently, something can be preserved in algebra and topology. I would be terribly interested to look at this picture.
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?
 A: Timothy Chow gave a fine answer in the context of classical mathematics. Here are some further sources for you to ponder. These not only work without choice, but also without excluded middle:

*

*Homotopy Type Theory: Univalent Foundations of Mathematics. For instance, is Blakers-Massey theorem advanced enough to count as real math?


*C-CoRN library, skim the README or see this paper for a humane summary of what is in it.


*UniMath library, inititiated by the late Vladimir Voevodsky, browse this folder to get a feel for what is in it.
The moral of the story is that the folk tales that mathematicians tell about how choice-free mathematics is completely different, or even impoverished beyond recognition, are just folk tales. Of course, one has to be a bit more careful, but that is always the case when we generalize, as new phenomena arise.
A: One of the standard texts which presents functional analysis only based on ZF+DC is the monograph (consisting of 3 volumes) Henry G. Garnir, Marc de Wilde, and Jean Schmets, Analyse Fonctionnelle.
Also in most of my monographs, in particular Topological Analysis, you will find many of the standard results of analysis and topology with explicit notes for which parts of the assertions more than ZF+DC is needed (and in a few cases also remarks when ZF alone is sufficient). Also in those of my monographs more related with integration and measure theory no use of anything more than ZF+DC is made unless explicitly mentioned. For nonstandard analysis the situation is different, although there are some recent papers that a certain internal nonstandard analysis can be carried out in ZF(+DC) as well.¹
In pure ZF (without DC) most of analysis is known to break down, in particular, it is almost impossible to do a reasonable measure or integration theory (as the real line might be a countable union of countable sets) or even topology (since sequential and topological definitions of a limit can differ already for functions of the real line).
Edit: ¹See e.g. Karel Hrbacek, Mikhail G. Katz, Infinitesimal analysis without the Axiom of Choice, Annals Pure Appl. Logic 172 (2021) (6)
A: ZF cannot prove the local equivalence between "epsilon delta" continuity and "sequential" continuity for functions on the reals.  A small fragment of (countable) AC does suffice for proving the equivalence.
In this light, most/many proofs in analysis would break down in ZF; a lot of work would be needed to sift through the details.
However, and in answer to your question, the aforementioned equivalence is provable in ZF for e.g. regulated functions.  Thus, for the special case of regulated functions, no (extra) AC is needed anywhere.
A more general answer (based on recent research) is the following: it seems that countable AC can be avoided if we require that all functions under study are Baire 1 (or effectively Baire $n$).
A: I agree with Asaf Karagila that the question as literally stated is a bit too sprawling, but you might want to start with Simpson's book, Subsystems of Second-Order Arithmetic.  Its goals aren't the same as yours, but along the way, the book shows how a large chunk of "countable mathematics" (whatever that means), including analysis, can be developed on the basis of second-order arithmetic (or even in $\mathsf{ACA}_0$), and a fortiori on the basis of ZF. Part of the trick is to avoid "overly general" statements of certain theorems; if you fix certain choices in advance, then you don't have to invoke AC to make those choices on your behalf later, and you can prove versions of (for example) Bolzano–Weierstrass that suffice for applications.
You might also want to check out another MO answer of mine which briefly discusses some other potentially relevant books. Again, they don't have exactly the same goals that you have, but the work they do may be relevant. Here's a quote from Bishop which gives some of the flavor:

Applications of the axiom of choice in classical mathematics either are irrelevant or are combined with a sweeping use of the principle of omniscience.  The axiom of choice is used to extract elements from equivalence classes where they should never have been put in the first place.  For example, a real number should not be defined as an equivalence class of Cauchy sequences of rational numbers; there is no need to drag in the equivalence classes.

It's harder to avoid AC when it comes to "uncountable mathematics" (whatever that means).  In another MO question, I asked whether Hahn–Banach for $\ell^\infty$ implies the existence of a non-measurable set.  The answer is apparently not well known, and perhaps is not known at all.  From this experience, I infer that analysts by and large have not even bothered to figure out in detail how much functional analysis can be carried out just on the basis of ZF+DC, let alone ZF on its own.
