Axiom of choice and calculus

I thought many results in calculus need axiom choice.
For example, I thought one needs AC to prove that a bounded sequence in the real line has a convergent subsequence.
Recently I was taught that one only needs mathematical induction to prove it.
So here are my questions.

Can most results in calculus be proved without AC?
If yes, what are the exceptions, to name a few?

Obviously a theorem which uses Zorn’s lemma most likely does need AC.
So please exclude obvious ones.

By “without AC”, I mean without any form of AC, i.e. countable or not, dependent or not. In other words, within ZF.

One of the motivations of my question is as follows.
People often unconciously use AC to prove theorems.
And it often turns out that their uses of AC are unnecessary.
For example, an infinite subset of a compact metric space has a limit point.
In his book “Principles of mathematical analysis”, Rudin proves this by choosing a suitable neighborhood of every point of the space.
He uses AC here, though he doesn’t say so.
However, since a compact metric space is separable, you can avoid AC to prove this theorem.

I’ll make the above statement clearer. You can even avoid countable AC to prove the above theorem.
In other words, you can prove it within ZF.

I’ll make my questions clearer and more specific.
By calculus, I mean classical analysis in Euclidean spaces.
Take, for example, Rudin’s “Principles of mathematical analysis”.
Can all the results in this book be proved within ZF?
If not, what are the exceptions?

Solutions Collecting From Web of "Axiom of choice and calculus"

To do classical analysis (i.e. things in $\mathbb R^n$) you don’t need the whole axiom of choice. Mostly you would need the axiom of countable choice, and rarely the stronger principle of dependent choice.

For example, the proof that continuity by $\varepsilon$-$\delta$ is equivalent to continuity by sequences (at a given point $x$) requires the axiom of countable choice.

We often use definitions by induction to define a certain sequence, the induction itself tells us that if we have defined $a_n$ we can define $a_{n+1}$ – so for a given finite number we can define a sequence longer that this number. We are usually interested, though, in the case where there is an infinite sequence, this is exactly where the axiom of choice comes into play. It tells us that there is such sequence and that we can use it.

However not everything requires the axiom of choice. For example the Heine-Borel theorem that states that closed and bounded intervals are compact (every open cover has a finite sub-cover) requires no choice whatsoever. Similarly a continuous function everywhere is sequentially continuous everywhere and vice versa (while requiring continuity at a single point at a time needs some choice).

Do note that general theorems about general functions/sequences/sets usually require some choice, on the other particular and very specific cases may be proved without it.

Some words to address the second edit: It is true that most of the people simply work in ZFC, and why shouldn’t they? It’s a very comfortable system and it saves you the need to verify certain things (e.g. if you want to use countable choice you have to keep checking that the families you choose from are countable). On the other hand it is also very true that most results people use require far less than the full axiom of choice, at least in elementary analysis.

Regardless to the above, once you get to functional analysis then the axiom of choice become more apparent (e.g. assuming the Ultrafilter lemma + Krein-Milman theorem implies AC in full). It is natural, too, that the larger your sets become the more choice you will need, and once you start talking about classes of spaces (e.g. all Hilbert spaces, or all locally-convex spaces) instead of a specific space – the more choice you will need to cover the general case.

Similarly in the “small” cases you can get away without choice (or with very very little) if you have a very specific case at hand. If, on the other hand, you want to prove a general theorem you might need to use some choice principle directly.

Doing analysis without any choice whatsoever is very hard and very limiting. I suppose it can be challenging and fun to people who find pleasure in that, much as I find pleasure in studying the possible structure of the universe without the axiom of choice. My suggestion is to examine your internal drive for this question: if you merely wish to learn on the axiom of choice and what is possible without it, I suggest picking up some books about mathematics and the axiom of choice:

  1. Herrlich, H. The Axiom of Choice (Springer, 2006)
  2. Moore, G. H. Zermelo’s Axiom of Choice (Dover Publications, 2012)
  3. Fremlin, D. H. Measure Theory, vol. 5 (Torres Fremlin, 2000)
  4. Schechter, E. Handbook of Analysis and Its Foundations (Academic Press, 1997).

If on the other hand you simply wish to reject the axiom of choice, and you have decided to work without it, I am certain there are references suited for that, alas I am unfamiliar with any of them.

Further reading:

  1. Continuity and the Axiom of Choice
  2. Foundation for analysis without axiom of choice?
  3. Terry Tao’s blog: Soft analysis, hard analysis, and the finite convergence principle.