I've been trying to get a handle on how higher order logic interacts with set theory. It's been stated convincingly that higher order logic with full semantics is set theory in sheep's clothing. For instance, an identity that is used for higher order Skolemization is equivalent to the axiom of choice.
If higher order logic with full semantics is just set theory, which set theory is it? NBG, new foundations, ZFC? Can we just pick any first order set of axioms for set theory and 'lift' them to higher order logic by interpreting the membership predicate? Where do the full semantics come from?