What we need perhaps is a hyperclass analogue of Myhill's theorem. en.wikipedia.org/wiki/Myhill_isomorphism_theorem

That is, to apply the hyperclass CSB, one usually has to know whether one can iterate infinitely in both directions, or only up, or only down. But even if each next thing is definable, we can't iterate it since the complexity grows with each step.

Ah, now I get your idea. But we can't use CSB for classes, since this is a meta-class instance. Hmmmnnn. But we are not going to be able to use meta-class CSB, since I worry that as you iterate things, the definitions get more and more complicated. For the usual CSB argument, you have to generate the iterates in both directions to tell which case you are in.

CSB works fine with proper classes---no choice required. But I don't really get how you intend to use it to solve the objection I raise. Could you explain?

We can't interpret a well order as coding independent bits like that, since all the bits might be 0, which would result in coding a definable class, and so if the bi-interpretation worked there would have to be a definable choice function.

@ElliotGlazer Sure, there are a huge number of different ways to do that, which is just half of it. The difficult bit is to show that every well order arises, and that the process composes to itself both ways. For example, it seems to me that we could definably change your well order by flipping those pairs suitably, so that the coded class of ordinals was empty. But in this case, it wouldn't be part of a bi-interpretation.

That would be only half of the bi-interpretation, namely, that every (rank-respecting) well order determines a choice function, which gives rise back to that well order in the way you describe. But for a bi-interpretation, we need it also to work for the other composition: every choice function gives rise to a well-order from which that choice function arises. (Using the same uniform definition in each direction for each composition.)

In particular, for a bi-interpretation, the definition of the well-order $\leq$ from the choice function $F$ must depend on every single value $F(x)\in x$, since otherwise there will be more than one $F$ giving rise to the same $\leq$, which prevents bi-interpretation.

@AsafKaragila That is how one usually makes a global well order from a global choice function, but the OP has already explained why this falls short of bi-interpretation. You need to define a global well-order which is equidefinable with the choice function and conversely, in a such a way that every global well-order arises.

This is a great question.

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.