Return to Revisions

No, because the latter theories has parametrically definable automorphisms that swap two equivalent classes, but the former theory is definably rigid (no need for class choice). If the theories were bi-interpretable, then we could fix a copy of the model with two equivalent classes (having the same elements), and inside this model we could define a copy of MK, and inside that define a copy of the original model, but because the automorphism would have to fix the definable interpretation but swap the classes, it would ruin the bi-interpretability feature.