14

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?

Sergei Akbarov
  • 7,274
  • 14
    This is way too open ended. – Asaf Karagila Sep 20 '22 at 11:49
  • @AsafKaragila I have added the tag "reference-request". – Sergei Akbarov Sep 20 '22 at 12:12
  • 3
    Yes, but you're asking "Hey, did anyone ever redo all of mathematics without choice?" and the answer is obviously not. There are some books, like Schecther's Handbook of Analysis and its Foundations which discuss some aspects of, well, analysis; Fremlin's Measure Theory has a part at the end of vol. 5 dedicated to, well, measure theory; and surely similar books exist in other fields. Herrlich has The Axiom of Choice which contains many possible disasters that may occur without choice throughout mathematics. But none of those is even remotely complete in any sense of the word. – Asaf Karagila Sep 20 '22 at 12:35
  • 2
    I like the question. A typical first course in undergraduate linear algebra doesn't use AC at all, as far as I know, since all the vector spaces considered there are finite-dimensional. In a typical undergraduate course in abstract algebra, I think you first encounter AC when you show that every commutative ring has a maximal ideal. I wonder how much of the standard material covered in such a course survives without AC. Presumably you have a lot of similar statements but with extra hypotheses, e.g. "Let $R$ be a commutative ring which has a maximal ideal." –  Sep 20 '22 at 12:48
  • @AsafKaragila: About "Did anyone ever redo all of mathematics without choice?": I have the impression that "anafunctors" in category theory are motivated by a desire to do something along those lines, at least for the many arguments in mathematics which have a clear category-theoretic formulation. My impression (as an outsider) is that "anafunctors" are a variant of functors, which behave well in the absence of AC, and replacing functors with anafunctors in many familiar category-theoretic arguments lets classical arguments go through without AC. https://ncatlab.org/nlab/show/anafunctor –  Sep 20 '22 at 12:54
  • 2
    @A.S. And even anafunctors will fail, eventually, in ZF, as you can see in https://mathoverflow.net/q/264585/7206, and even if they don't, the question still feels broad. – Asaf Karagila Sep 20 '22 at 13:01
  • 1
    @A.S. linear algebra uses the results of the theory of real numbers which is usually constructed inside the axiomatic set theories like ZFC. I think it's impossible to say that linear algebra does not use the axiom of choice. – Sergei Akbarov Sep 20 '22 at 13:08
  • @AsafKaragila: I did not expect that somebody rewrites "all of mathematics" without choice. This could be done in some fields. As an example, Kushner shows what the intuitionists point of view gives in analysis. I would think, that the people who discuss the "validity of the application of the axiom of choice here and there" could do something similar in this direction. Does your "answer is obviously not" mean that there are no reviews of what happens in Algebra, Topology, or Analysis? – Sergei Akbarov Sep 20 '22 at 13:42
  • @AsafKaragila and as a specialist in this field you could clarify this: "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?" – Sergei Akbarov Sep 20 '22 at 13:43
  • 2
    @SergeiAkbarov: Certainly you can find a lot of information as to what can happen in algebra, as I remarked, Herrlich's book contains a lot of information. On all three fields, actually. I've also mentioned Schechter's book in a previous comment, as a source for analysis, etc. As for the second comment, I'm not sure what is unclear. Asking if we can prove that compact subsets of the real line are closed can be done with or without the axiom of choice, but do you really need to rewrite classical analysis and basic topology in ZF for that? – Asaf Karagila Sep 20 '22 at 14:16
  • @AsafKaragila thank you for the references, I'll look at this. As to compact subsets I even don't see if this question still makes sense in the situation when we drop the axiom of choice. After all, in this case, the (usual) theory of the real numbers must also be thrown out, and I do not even understand what kind of examples of topological spaces remain. Does it make sense to be interested in their properties, if the examples known to you disappear, and you don’t understand what others are? If these examples are anything trivial or absurd, how can such a theory be interesting? – Sergei Akbarov Sep 20 '22 at 14:45
  • What is surprising in these debates is the willingness of people to discuss mathematical questions beyond the framework of the mathematical approach, metaphysically, in Hegel's style. One would expect that a person first constructs a theory with examples and problem statements that would convince the audience that this is really interesting, and only then he proves deep theorems about the objects of this theory. But here we see a situation where even the list of examples is not clear what. – Sergei Akbarov Sep 20 '22 at 15:11
  • Also, when you find a "constructive proof" of X, the viewer can't check that the Gentzen tree of your reasoning doesn't really contain the axiom of choice, because this tree breaks at the lemmas you use. In a "linearly built" theory, the viewer can look at the proof of the previous results and make sure that everything is clean there, but in your situation you don’t have a "linear theory". – Sergei Akbarov Sep 20 '22 at 15:11
  • 1
    @SergeiAkbarov: I think you are veering too far into philosophy, even for my taste. And I'm not even sure that this is still mathematical philosophy at all, rather than just general philosophical approach to the logic used in proofs and formal statements. I don't know if this is a fruitful area of mathematical work, to be honest. I'm happy to have discussions about philosophy, as most people who had a few beers with me will testify, but to say that somehow the fact we omitted an axiom that was irrelevant to the definition requires us to re-examine everything? That might be going too far. – Asaf Karagila Sep 20 '22 at 15:49
  • @AsafKaragila in my understanding, on the contrary, I try to remove philosophy from mathematics. All mathematical theories are built inductively: first people list the rules of the game, and then they play the game. Only in logic everything is not like in the other mathematics. But still, what examples of topological spaces remain if we exclude the axiom of choice? – Sergei Akbarov Sep 20 '22 at 16:02
  • 1
    Where do you think topology is being used when you *define* topological spaces? – Asaf Karagila Sep 20 '22 at 16:50
  • This sounds a little bit like a "tell me about logic" question. It might make more sense to single out a specific theorem and ask what remains of it, when you use other, specific logical foundations. – Ryan Budney Sep 20 '22 at 17:18
  • @AsafKaragila, I don't see problems with the definition of topological spaces. But if we throw away the theory of real numbers (and the axiom of choice) what examples of topological spaces remain? – Sergei Akbarov Sep 20 '22 at 17:19
  • @RyanBudney I expected that people who are arguing about "constructive proofs" have already accumulated a list of examples. I didn't see it. – Sergei Akbarov Sep 20 '22 at 17:24
  • 2
    (1) Where in the definition of a topology do the real numbers come in? (2) Where in the definition or construction of the real numbers does the axiom of choice come in? – Asaf Karagila Sep 20 '22 at 17:35
  • @AsafKaragila (1) I did not tell that real numbers manifest themselves somehow in the definition of topological spaces; (2) but I used to think that in the standard construction of real numbers in axiomatic set theories like ZFC (in the sequence $\mathbb{N}\to \mathbb{Z}\to \mathbb{Q}\to \mathbb{R}$) the axiom of choice is used, for example, when people use the fact that the set of finite ordinal numbers $\mathbb{N}$ is well-ordered. Is that not true? – Sergei Akbarov Sep 20 '22 at 17:50
  • 4
    @SergeiAkbarov: It is very not true. No. It might be wise, before starting with mathematics without AC, to learn a bit of wet theory without AC. For that Jech's Axiom of Choice book is pretty decent. Azriel Levy is known to keep track of it, so I imagine that his book in Basic Set Theory would be good as well. – Asaf Karagila Sep 20 '22 at 18:11
  • @AsafKaragila so if I understand correctly, this means that the theory of real numbers is not changed when we throw away the axiom of choice? – Sergei Akbarov Sep 20 '22 at 18:14
  • Ah, the idea is that the theory is changed, but the examples of topological spaces constructed from real numbers do not disappear, they are preserved but with some different properties. – Sergei Akbarov Sep 20 '22 at 19:31
  • @AsafKaragila as far as I understand, in this "constructive topology", the definition of compact space breaks down into two non-equivalent ones: the definition by open sets is not equivalent to the one where nets are used. That is, the same effect is manifested here as in constructive analysis by Kushner: definitions break down into different non-equivalent ones. I foresee that when someone honestly writes a textbook on such a topology, people will stop arguing about the axiom of choice, being horrified by the picture that has opened up. – Sergei Akbarov Sep 21 '22 at 05:38
  • 6
    @SergeiAkbarov: you confidently made a host of claims about how all sorts of mathematics "breaks down" and "nothing can be done" without the axiom of choice, which is simply false. I would urge a more cautious approach that doesn't irk people who actually know what can be done without AC and will simply ignore you as they're tired fighting this particular combination of ignorance and arrogance, driven by unchecked confirmation bias. – Andrej Bauer Sep 21 '22 at 06:33
  • @AndrejBauer I did not say this: "all sorts of mathematics "breaks down"", nor this: ""nothing can be done" without the axiom of choice". And I also have eyes and notions of decency, and it's not my fault that the simple-minded question "what happens if AC is removed from the list of axioms" is irritated by people constantly discussing "what happens if AC is removed from the proof of X, Y, Z". – Sergei Akbarov Sep 21 '22 at 13:39
  • You could notice that this is actually a big problem: to understand what people in a club mean when they say something, it often happens that you need to ask them a question that they by some strange regularity find indecent. And sometimes this leads to wrong quotations. – Sergei Akbarov Sep 21 '22 at 13:39
  • To the people voting to close this question: wouldn't it be more honest to leave this thread for non-specialists, among whom certainly there are people who (like me) are interested in textbooks on analysis in ZF? – Sergei Akbarov Sep 21 '22 at 14:02
  • 1
    @SergeiAkbarov – Here is an off-putting remark of yours: "I foresee that when someone honestly writes a textbook on such a topology, people will stop arguing about the axiom of choice, being horrified by the picture that has opened up". The confirmation bias is amazing. – Andrej Bauer Sep 21 '22 at 14:29
  • @SergeiAkbarov: and another one was "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." You make your judgements before you even find out what the evidence is. – Andrej Bauer Sep 21 '22 at 14:30
  • 1
    @SergeiAkbarov: so I think this would make a fine question if you edited it so that you genuinly ask the question without prejudice and insinuation as to what the conclusion of the answer must be. – Andrej Bauer Sep 21 '22 at 14:41
  • @AndrejBauer "I guess" is a speculation, not a judgment. And "I foresee" was after Asaf's explanation about $\mathbb R$ without AC, this already gives enough grounds for judgment. Because it crosses out all the theorems from the standard list of questions for the analysis exam. – Sergei Akbarov Sep 21 '22 at 14:43
  • @AndrejBauer I can rewrite, but I actually don't feel what is wrong. You can suggest. – Sergei Akbarov Sep 21 '22 at 14:45
  • @AndrejBauer I think our misunderstanding of each other comes from the fact that we hear discussions of these issues in different companies. You, as a specialist, hear the arguments of other specialists, and this does not cause rejection, because specialists understand each other. And I, as a non-specialist, hear this mostly from other non-specialists who follow the meaningfulness of what was said very poorly, and this revolts me. And some of that outrage is reflected in my posts in the MO. – Sergei Akbarov Sep 21 '22 at 14:50
  • @SergeiAkbarov: point taken. As for rewriting, just water down statements in which you imply, suggest, guess, or predict that horrible things happen once we remove the axiom of choice, because that's not true and it's tiresome to listen to such sentiments. – Andrej Bauer Sep 21 '22 at 15:19
  • @AndrejBauer ok, I'll correct the text, but later, because I was working today, and I am a bit tired. – Sergei Akbarov Sep 21 '22 at 15:33
  • 1
    A technical remark about a previous comment: compactness (without AC) seems to be defined in terms of open covers. Instead of nets, you can use filters, which leads to an equivalent definition without AC (nets are somehow choicy by the external nature, but filteres are intrinsic). – Z. M Sep 21 '22 at 16:24
  • @AndrejBauer I corrected the question. I will not touch the comments, because there is no possibility to edit them, and besides this it seems to me they are not very important. – Sergei Akbarov Sep 22 '22 at 00:06
  • 8
    Minor comment, but no one's brought it up yet: Absoluteness results from set theory imply that AC cannot be necessary to prove sufficiently simple statements. For example, Shoenfield's absoluteness theorem implies that if you can prove, using AC, a statement of the form "for all $X$ there is a $Y$ such that $\varphi(X,Y)$" where $X$ and $Y$ range over sets of integers and $\varphi$ only quantifies over integers, then you can prove it without using AC. Many theorems about countable objects can be put in this form—my favorite example here is Hindman's theorem—so they're all preserved in only ZF. – Kameryn Williams Sep 22 '22 at 21:51
  • 3
    @KamerynWilliams Shoenfield absoluteness is enough to show that $\Pi^1_4$ theorems of ZFC are provable in ZF. If ZFC proves $\forall X\exists Y\forall Z\exists W\phi$ (with $X,Y,Z,W$ ranging over reals and $\phi$ arithmetical) then to prove it in ZF, let an arbitrary $X$ be given, work in $L[X]$ (which satisfies ZFC) to get some $Y\in L[X]$ satisfying $\forall Z\exists W\phi$ in $L[X]$. By Shoenfield absoluteness, the same $Y$ works in the "real world". – Andreas Blass Nov 18 '22 at 01:13
  • 2
    The argument in my comment above is, I believe, in Platek, Richard A. Eliminating the continuum hypothesis. J. Symbolic Logic 34 (1969), 219–225. Despite the title, it also contains a lot about eliminating AC. – Andreas Blass Nov 18 '22 at 01:18

4 Answers4

22

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.

Timothy Chow
  • 78,129
  • Tim, "on the basis of ZF" - does this mean that Simpson turns ZF somehow into a second order theory? – Sergei Akbarov Sep 20 '22 at 19:23
  • 1
    I would say it this way: second-order arithmetic is interpretable in ZF. The theorems of second-order arithmetic, so interpreted, are theorems of ZF. – Timothy Chow Sep 20 '22 at 22:30
  • A second order theory is interpretable in a first order theory? The universe of this interpretation, is it the usual $\mathbb N$? – Sergei Akbarov Sep 21 '22 at 05:03
  • Tim, I guess the universe must be different, not the usual construction of $\mathbb N$. And real numbers must be also different, not the usual $\mathbb R$ as it is normally constructed in ZF, because otherwise we would get that Bolzano-Weierstrass holds in the usual $\mathbb R$ without the axiom of choice. – Sergei Akbarov Sep 21 '22 at 06:12
  • 1
    @SergeiAkbarov The terminology "second-order arithmetic" may be slightly misleading; it's really a two-sorted theory that is still based on first-order logic. One sort is natural numbers and the other sort is sets of natural numbers. It's called second-order because you can quantify over sets of natural numbers and hence over real numbers, but $\mathbb{R}$, thought of as the set of all subsets of $\mathbb{N}$, is not something you can refer to directly. Chapter 1 of Simpson's book is available online; I refer you to it for more details. – Timothy Chow Sep 21 '22 at 12:08
  • Tim, yes, I am reading this, but you know, this is not what I expected. This is not the same as removing AC from ZFC. – Sergei Akbarov Sep 21 '22 at 13:09
  • 4
    @SergeiAkbarov Correct. But I think the point is that if you're serious about getting rid of AC, then the way to go about it is not to begin with classical mathematics, hunt around for uses of AC, and see if you can pull out AC like a Jenga piece without causing the whole tower to collapse. The way to do it is to rebuild mathematics from the ground up. Since nobody seems to have done exactly what you were hoping for (building math using ZF), the closest thing is to see how various people have developed large portions of mathematics without using AC. – Timothy Chow Sep 21 '22 at 13:18
  • 1
    Tim, I understand what you mean, but before doing what you say, the first step for me would be an attempt to see what happens if I pull out the brick that everyone is trying to pull out. – Sergei Akbarov Sep 21 '22 at 13:50
11

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)

Martin Väth
  • 1,839
  • I'm not sure that "In pure ZF ... it is almost impossible to do a reasonable measure or integration theory" is quite correct. There are difficulties, to be sure, but Bishop already took a stab at developing measure theory without choice. See also Constructive algebraic integration theory without choice by Spitters and Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory by Petrakis and Zeuner. – Timothy Chow Sep 24 '22 at 20:57
  • 5
    Without any choice what you get does not really resemble the classical setting. Lebesgue "measure" is not $\sigma$-additive, for instance. It is true you can "recover" more than one would expect. Fremlin has an interesting approach using "codes" of sets rather than the sets themselves. – Andrés E. Caicedo Sep 24 '22 at 22:16
  • 3
    @TimothyChow ”almost impossible” was probably a bit too harsh, but you have to be extremely careful which definitions you choose. So there is not “the” integration theory anymore in ZF, but several such theories, usually preserving different properties (compared to the ZF+DC situation which has all properties and in which all approaches are equivalent, at least for the Lebesgue measure). – Martin Väth Sep 25 '22 at 15:02
  • @MartinVäth I realize that I'm confused about your comment regarding nonstandard analysis. Shouldn't there be some kind of transfer principle that means that the apparent use of stronger axioms isn't really necessary? Admittedly, I'm not very familiar with nonstandard analysis. – Timothy Chow Aug 02 '23 at 01:09
  • 1
    @TimothyChow: In nonstandard analysis of Robinson/Luxemburg, the transfer principle applies, roughly speaking, only to standard sentences; but there are more. You can “explicitly” define non-measurable sets there. For instance, let $f\colon[0,1)\times\mathbb N\to{0,1}$ be such that $f(x,n)$ is the $n$-th digit of the binary expansion of $x$. Then for any infinite hypernatural $h$ the set ${x\in[0,1):{}^f({}^x,h)={}^*1}$ is not Lebesgue measurable. It is surprising that this set cannot be defined in the restricted languages of internal set theory from the cited paper of Hrbacek-Katz. – Martin Väth Aug 05 '23 at 21:27
  • @AndrésE.Caicedo When you say "Fremlin," I take it you mean his multi-volume treatise, Measure Theory? That's a dauntingly long text. Can you point to the most relevant sections for the present topic of discussion? – Timothy Chow Aug 21 '23 at 14:42
  • @Timothy I didn't mean any specific text, but yes, you can find details in volume 5 of the book you mention, particularly Chapter 56. – Andrés E. Caicedo Aug 22 '23 at 18:01
9

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$).

Sam Sanders
  • 3,921
  • 4
    It is very important to point out that this failure of equivalence is only when talking about "a single point", and a function that is everywhere sequentially continuous is also everywhere continuous. – Asaf Karagila Sep 27 '22 at 00:59
  • Hence the "local" equivalence I mentioned, but you are of course right. – Sam Sanders Sep 27 '22 at 07:14
  • Just a reference for 'Baire 1/Baire n' functions, since I had to look it up: https://en.wikipedia.org/wiki/Baire_function – David Roberts Nov 18 '22 at 02:24
8

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:

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.

François G. Dorais
  • 43,723
Andrej Bauer
  • 47,834
  • 3
    Andrej, you misunderstand me all the way. I did not say that the orthodox foundations are better than others. I was trying to understand what happens if we remove AC from ZFC, this is not the same. – Sergei Akbarov Sep 21 '22 at 14:54
  • Thanks for your remark, I edited the paragraph to address your question more directly. It's not easy to give a precise technical answer, though, because you're asking about "all math". – Andrej Bauer Sep 21 '22 at 15:20
  • Just for my own education, I take it that Blakers-Massey for simplicial sets (not just the "synthetic" form of Blakers-Massey) can also be proved without AC or LEM? – Timothy Chow Sep 21 '22 at 17:14
  • 3
    @TimothyChow: that's probably hard to figure out, as classic proofs are unlikely paying attenition to where and whether there are essential uses of AC and LEM. But already showing the basic categorical structure of Kan simplicial sets is tricky without LEM – this was a stumbling block for a long while in HoTT, and was resolved by passage to cubical sets. – Andrej Bauer Sep 21 '22 at 20:43
  • One should add that the various attempts to develop (Bishop style) constructive math without (countable) AC have largely dwindled. One can of course do certain theorems/parts of constructive math without any AC, but in the end it seems a lost cause (correct me if I am wrong). – Sam Sanders Sep 27 '22 at 07:18
  • 2
    @SamSanders: Bishop-style constructive analysis does indeed rely on countable choice (Dependent choice). Choice-free analysis uses Dedekind reals, and is less well-developed, although there is some amount of it. For instance, the HoTT books develops the basics without choice, and there are others. It's easier to do general topology without countable choice. Choice-free algebra has been studied quite a bit and it has its own set of challenges. – Andrej Bauer Sep 27 '22 at 09:24