Does this mean using Henkin semantics doesn't require choice then, because first order theories don't require choice for Skolemization and Henkin semantics essentially makes higher order theories multi-sorted first order theories?

I don't know that it's obviously full choice and not something weaker like countable choice, since first order theories have countable models. As someone who is a not a mathematician, choice always being required for any Skolemization is acceptable as an answer, but I find it a bit surprising given how readily I use Skolemization for my proof calculus.

Thanks, I'll check it. I was mostly motivated in asking questions about satisfiability, decidability, and provability about questions inside an automated theorem proving system, so I need to be able to formalize all definitions if I want to ask a question about a particular well formed formula like "Is this a decidable statement?" or "Is this a satisfiable statement?" or "Do statements that have this form fall in the set of decidable statements?"

The definition of a Gödel numbering is done in the metatheory, along with other definitions for making informal proofs. I'm looking for formal first order definitions, including of Gödel numberings. Arithmetic is embedded in set theory, but without the appropriate definitions its hard to ask questions about arithmetic in raw set theory, and without the appropriate definitions in arithmetic, its hard to ask questions about Gödel numbering of formula in arithmetic.

Are you saying that you can't use it to factor or solve discrete log in non-associative unique factorization domains like the 'Cayley integers' of the octonions, or is that just a comment that I'm abusing terms with the wrong definitions? I thought Shor's algorithm wouldn't apply to quaternions since it supposedly works on finite Abelian groups, but Julia Upton demonstrates that you can apply it to quaternions by (somehow) extracting an Abelian subgroup of quaternions and then applying Shor's algorithm.