I've been reading about the Axiom of Choice, and my current understanding is that we can assert a choice function exists even in cases where it may be impossible to construct a deterministic formula that produces the behavior we're looking for. This confused me at first (how can you have a function you can't write down?) but then I remembered that functions can be understood both intensionally (as a formula) and extensionally (as a set of ordered pairs), so I assume that these undefinable choice functions must exist in a purely extensional form, devoid of intensional content.
If this understanding is correct, is there a specific term for these non-intensional functions? Or are these arbitrary mappings so common that there's no need to treat them as a special kind of function?
Also: would it be correct to say that the Axiom of Choice is required if and only if we need to apply a choice function to an infinite number of sets and no intensionally-defined function is available?
Mathematics, as we perceive it, is kind of funny.
We start by learning about functions which are continuous and differentiable, and we see an example (maybe Weierstrass' function) of a function which is continuous but nowhere differentiable. And we call that one a pathological function.
Or we learn about Borel and Lebesgue sets, and we learn about Vitali sets as an example of non-measurable sets. And we call these pathological.
But the reality in mathematics is quite different. Most functions from $\Bbb{R\to R}$ are nowhere continuous, most of the continuous functions are nowhere differentiable, and most differentiable functions are nowhere continuously differentiable, etc. Similarly, most sets are not Borel, and most sets are not Lebesgue measurable. (In all of these cases we can give the word "most" a very concrete, and a very real meaning.)
This means that the continuous functions are the exception. We focus on these exceptions because we are looking for order in all of this chaos. But the truth is that "irregularity", as we want to think about it, is the common law of the land.
Okay, so why am I even bringing this up? Well. You seem surprised that a function can exist without a formula which defines it. But in some sense, that is "more reasonable". Yes, there are subtle meta-mathematical points about mathematical universes where everything has an explicit definition (and the axiom of choice holds there, of course). But these are the exception, not the rule.
The goal of defining a function by a set of ordered pairs, rather than an explicit formula, is to do two things:
Formulas (in set theory) are not mathematical objects, they are meta-mathematical objects.1 We want to be able to define the notion of a function in the universe, which means that it needs to be an internal property of a set. For example, being a set of ordered pairs with a certain property.
When we abstract the idea of a function, we see that it is not about the formula, but rather about the uniqueness of an output. Sets of ordered pairs are exactly what we need to model this idea. Now we can talk about functions abstractly. Just like we can talk about real numbers as an abstract idea, without having to specify their entire decimal expansion.
Finally, on your tangential question on the use of the axiom of choice, I'd think it's best to avoid "if and only if" here. It can be misleading, and putting hard lines in the sand before you've developed the correct intuition will end up causing more issues than not. You're right, that choice is necessary exactly when we need to choose from infinitely many sets, since ZF proves that any finite family of non-empty sets admits a choice function. And indeed, in some situation we can define a choice function "by hand" and thus avoid relying on the axiom itself (e.g. the minimum of a set of natural numbers). But there is a reason why many staunch opponents to the axiom of choice were actually using it implicitly (or rather, using weak forms of it implicitly).
One prominent mathematician told me once that the hallmark of a good foundational theory of mathematics is that you don't notice when you're using it. That is to say, it gives you the freedom to focus on the mathematics. The axiom of choice fulfills this exact criteria most of the time. So I'd say that your idea is correct, but you shouldn't be putting "if and only if" in there. Instead take it as a guiding intuition to start with.