Upon rereading the question, I sense there may be a terminological or conceptual confusion in play.
The terms “second-order logic” and “higher-order logic” are unfortunately used to denote two vastly different things:
Proper second/higher-order logic. This is a semantically defined system; its models consist of a first-order structure to interpret the first-order sort, which is canonically expanded to higher sorts by taking power sets and/or sets of all functions with appropriate domains (depending on the exact language). In this case, validity of the $$\tag{$*$}\forall x\,\exists y\,\phi(x,y) \leftrightarrow \exists f\,\forall x \,\phi(x, f(x))$$ schema in this logic is equivalent to the axiom of choice, as noted in Asaf’s answer. This is not limited to the axiom of choice: a substantial number of other set-theoretic principles (e.g., (non)existence of various large cardinals) are equivalent to validity of particular formulas in second-order logic, so this logic is effectively set theory in disguise. For much the same reasons, it has no proof system (its complexity is much higher than recursively enumerable).
Various first-order theories formulated in the multi-sorted language of second/higher-order logic. The fact that the question refers to “proof calculus” strongly suggests that this is the intended meaning here.
In this case, the schema $(*)$ is just a convenient axiom that one might or might not choose to adopt in a particular system. The fact that it may be invalid in “standard models” as in 1. if the axiom of choice fails is neither here nor there: the logic is in any case not complete with respect to standard models, and there is no particular need for it to be sound either.
Since these theories are generally recursively axiomatized, typical questions about their proof-theoretic properties (e.g., whether including the choice schema $(*)$ significantly strengthens a given system, or whether it is conservative for some class of formulas) are arithmetical statements of low quantifier complexity. As such, they are absolute, and in particular, they do not depend on whether the axiom of choice holds in the metatheory.
However: to further terminological confusion, the schema $(*)$ is itself called the axiom of choice in the context of these logics. So, it is not actually clear to me what you are asking about: does the “require the axiom of choice” in the last paragraph of the question refer to the axiom of choice in metatheory, or to the schema $(*)$?