But the tree property alone is not equivalent to weak compactness even in ZFC, unless one also specifies that the cardinal is inaccessible. But $\omega_1$ is never inaccessible.

There are over a dozen common characterizations of weak compactness in ZFC, but they are not all equivalent in ZF+DC, so could you let us know which version of weakly compact you want?

@JeanneScott I'm not sure---seems like a good question to ask on MathOverflow!

Here is a link to reviews of Felgner 1971 and a paper of Mostowski, which give the argument: doi.org/10.2307/2272004. But I think the argument is now quite commonly given by just explaining how the forcing goes. Since the forcing adds no sets at all, it is amongst the easy kinds of class forcing. I'm not sure if the argument is in Jech. Solovay says on FOM (here: cs.nyu.edu/pipermail/fom/2010-April/014533.html) that the result is due to many people, including himself, and Jensen.

Thus, one need only check that GBC holds in the forcing extension, where the new classes are obtained by old classes that are names. These are the same as classes that are definable from the new well order. I'll try to find a reference.

I'm not sure what the best reference is for the forcing argument. The basic fact is that GBC with global choice is conservative over ZFC. To see this, if you have any ZFC model, then it is easy to see that you get GB+AC in the second-order structure by allowing all definable classes (with parameters). The only thing remaining is global choice, which might not hold if there is no definable global well order. But the forcing P with set-sized condition well ordering an initial segment is class forcing adding a global well order. This forcing notion is very mild, since it adds no sets.

Genericity is not needed when $\kappa$ is inaccessible, since in this case you can use the full second-order part $V_{\kappa+1}$, and you'll therefore get not just GBC but fully Kelley-Morse set theory, which allows quantification over classes in the comprehension scheme.

Oh yes, I see that we hit upon the same idea.

Yes, I see the certain affinity—thanks for the link. One difference, however, is that $\kappa$ is regular in his argument, whereas the difficulty of the worldly case is that they are singular in the hard case. This is why the method of working along the $\Sigma_n$-correct cardinal sequence is used.

Possibly related: mathoverflow.net/q/15841/1946

Mike and Asaf, yes, that is right. Except that the argument isn't "adding" the generic well order $\leq$ of $V_\kappa$ by forcing over $V$ to add it in the usual forcing manner, but rather proving that there is already in $V$ such an order that is $\text{Def}(V_\kappa)$-generic, and this is enough to get NBG in $\langle V_\kappa,\in,\leq\rangle$, just in in the usual conservativity argument for NBG over ZFC. So we can freely add a global choice order to any worldly cardinal and preserve NBG.

Good question! However, if the perfect set property holds for every uncountable projective set (this is a consequence of PD), then every definable set you are talking about would be either countable or size continuum, in which case equicardinality would be expressible, but CH needn't hold.

Yes, that is right. You can express countability directly, in the style of my answer, and so if there is only one other cardinality, then you can also express that. If CH fails, however, then we cannot (provably) express the different cardinalities, since forcing can make them the same without adding reals and therefore without changing second-order arithmetic.