A late reply, but hopefully late is better than never.

Sort of. I think talking about it as if it's a phenomenon unique to sets (although indeed things are ultimately traceable back to the close relationship between second order logic and set theory) obfuscates things somewhat.

Let's take a step back. You give me a theory (second order Peano Arithmetic, let's call it PA2). Let's call the unique model (from the point of view of the metatheory) that satisfies PA2 N. Let's call our metatheory T and the implicit background model of T M.

We decide to test whether we both have the same N by asking whether N satisfies a sentence s in the language of PA2.

It turns out that whether N satisfies s depends on a theorem t that is independent of T. Do we agree on the same N? Perhaps we have different M that respectively do and don't satisfy t.

Okay that's fine, maybe our different M can be unified under a single M* that subsumes both to give us a definitive answer on N. Unfortunately it turns out that as we look at increasingly larger M* the answer of whether N satisfies s flips back and forth. There is no universal M* we can appeal to.

That's basically what's going on here when I say that all second-order logic has done is push ambiguity to the metatheory (and metamodel).

Now you can maybe argue that second-order logic is at least less ambiguous. After all the overall structure of N is assured right? We don't have non-standard natural numbers right? Well this is a bit tricky to say. Perhaps our metamodel M is actually ill-founded (which is possible from the perspective of a metametatheory even if it satisfies something like ZFC), causing N to have non-standard natural numbers as well. Now there is the possible objection that if you mess with the metamodel all bets are off. But the problem is that second-order logic with full semantics, because it lacks completeness, constantly relies instead on the metatheory and by extension metamodel to actually do proofs. That is you rarely have interesting, new proofs in second-order logic, but rather meta-proofs using the metatheory. So it is totally fair game to start examining the metamodel if everything you're doing is meta-proofs!

Moreover, from my perspective as someone who disagrees with strong, mono-universe Platonism (a term I made up that refers to people who believe that every axiom has an objective truth value and we cannot "choose" axioms in any real sense but rather are only on a journey to discover the "true" axioms of mathematics), giving up completeness is a really hard pill to swallow.

This makes it really hard to understand notions like "independence" and "consistency." If we lose completeness, consistency is no longer a sufficient criterion to admit a theory, which makes it hard to define something like independence. If we say both t and Not(t) are consistent with T, does that mean both t and Not(t) perfectly admissible axioms to add to T? The answer in the absence of completeness is no. We must investigate further. And in the case of categoricity such as with PA2, the answer is a definitive no. Only one can be admissible not both.

This can lead to really strong philosophical positions that I disagree with. For example, ZFC2 (second-order ZFC) is categorical. So either CH or Not(CH) is "true." But both are potentially consistent with ZFC2 (I'm handwaving this because second-order logic losing completeness makes even talking about consistency kind of weird unless you have completeness for your metatheory and metamodels).

But CH seems to me so clearly artificial. It's just a weird artifact of random cardinals we've made up. You're telling me that I'm either allowed to use it or not allowed to use it, but we don't know which? That seems way too strong to me.

This is especially problematic if we think back to M* where it's not clear at all when we should stop going up the hierarchy of M*s, since our answer keeps going back and forth.

That's why although I'm okay with second-order logic as a formal tool, I prefer to think in a metatheory that embraces completeness (you'll see I did that when I started talking about t being independent of T), which usually ends up being some version of FOL. Otherwise I think it's very difficult to work with mutually incompatible mathematical axiom sets for different problems since you're basically assuming completeness at a philosophical level when you do that.

At the end of the day, from my point of view, while models are important tools for examining mathematical theories as objects in their own right, the realm of formal mathematics is proofs. I hold the ability to completely formalize an argument in a computer, even if to actually do so would be extremely tedious and even impractical, as my standard for mathematical proof. A proof that is actually impossible to completely formalize constitutes "hand-waving" for me.

By that philosophical standard, we must have completeness because we are putting proofs first. This is what Vaananen means when he says that we realistically can't choose between full semantics and Henkin semantics if we wish to use second-order logic for mathematical foundations. If you want to preserve that sort of rigor, you really do need completeness and by extension you really need to default to Henkin semantics, which ends up just being multi-sorted FOL.