The title is the question. I apologize if this is a naive question. I know there are weaker versions of AC, but this is not what I am looking for. For example, is there a theorem that its proof invariantly requires TWO uses of AC? I don't know how to make it more precise. Thanks in advance.
Context: When proving "Sequentially compactness implies compactness", it looks like there are two instances of AC, for concreteness, let's say we adopt the "Lebesgue Number" approach. Then we need the following two lemmas:
- Sequential compactness implies Lebesgue's Number Lemma.
which requires Axiom of Countable choice, see here.
- Sequentially compactness implies total boundedness of metric spaces.
which again uses ACC, see proofwiki.
It seems whatever approach we choose, there must be two instances of AC. So can we formalize this? Of course, given AC available, we can use it arbitrarily many times. But some mathematicians will intentionally reduce the use of it as much as possible. This leads me to question if there is a notion that quantifies the dependence of AC, or any axiom in general.