# Is there a notion that quantify the dependence of a proof on AC?

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:

1. Sequential compactness implies Lebesgue's Number Lemma.

which requires Axiom of Countable choice, see here.

1. 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.

• I think there is an effort to reduce the level of choice required, because that gives a stronger theorem. The best is to use no choice at all, so it is a theorem of ZF. Once you use a certain level of choice, you can use it as much as you want because it does not strengthen your assumptions to use it again. – Ross Millikan Jan 20 at 4:25
• Yes, but even given AC, they will try to reduce the uses as much as possible. – YuiTo Cheng Jan 20 at 4:28
• I think you may be over-generalizing. I bet there are mathematicians who do not make the slightest effort to avoid using the axiom of choice. – bof Jan 20 at 5:11
• This is a great question! Not an answer, but: lower down in the hierarchy of theories, Weirauch reducibility and its relatives can be used to study the number of times a mathematical principle is invoked during a proof - roughly by casting everything in computational terms (so principles are replaced with algorithms). Some issues crop up in higher-level contexts (e.g. set theory), but you may still find the general idea interesting. – Noah Schweber Jan 20 at 5:36
• By fixing a choice function on a large enough set, you effectively reduce all your uses of choice into one. Because once you've fixed that choice function, the rest is given. – Asaf Karagila Jan 20 at 7:29