@PeterLeFanuLumsdaine I took Qiaochu to be referring to our existence in physical reality, which does break the symmetry, since our bodies are not fully symmetric. Meanwhile, I agree that it is essentially the same problem to produce a 2-element set without a privileged element. My point is that to exhibit such a set (without just assuming it by fiat) we typically do so by forgetting structure rather than by having direct access to such a structureless symmetric set.

Our experience of any plane in physical space does privilege a particular orientation, since we inevitably find ourselves on one particular side of it. And I find this to be an instance of the phenomenon I am speaking about, whereby we typically construct nonrigid mathematical structures from rigid ones by forgetting structure, rather than constructing rigid structure from the nonrigid by making symmetry-breaking choices. (Of course, we can do this latter process, but only after having already previously constructed the nonrigid structure from a rigid structure.)

@QiaochuYuan Your idea relies on having already the Euclidean plane itself as a vector space. How do you construct that (in ZFC, say) without in effect already breaking (and then forgetting) the symmetry?

See also my related essay on the natural attitudes that one might take on the complex numbers. Many people favor a vision with a fundamental symmetry between $i$ and $-i$, and yet I know of no construction of that structure that doesn't proceed through the rigid conception, which in this sense, I is seminal. That is, we don't begin with the naked structure and then arbitrarily impose a choice, but rather construct the rigid structure and then forget some of it. infinitelymore.xyz/p/complex-numbers-essential-structure

OK, I see now. You are regarding every $r\in\mathbb{R}$ as it sits in No, and so has nonstandard $n_\alpha$th digit.

In the definition of $X_\alpha$, you do not refer to $\alpha$, and you do refer to $n$, and so I am unsure exactly what you mean. Also, you refer to translation by standard dyadic rationals, but since it is a set of reals, standard is all that is available. I have a feeling you may intend to define $X_\alpha$ in No using $n_\alpha$. Is that right?

Oh, I'm not doubting the statement, and I shall look forward to what you write. I was merely objecting that it doesn't make sense to say that global choice is equivalent to a statement that is not expressible. I guess what is meant is that global choice will be equivalent to an instance of that statement that is expressible. (Note that even with global choice, we cannot in general get satisfaction classes for a class model, although I think the saturated/indiscernibility idea may provide the desired satisfaction class for the case that is needed.)

@ElliotGlazer I don't see that the assertion "any two PCS models of a complete theory T are isomorphic" is expressible in set theory. Proper class models do not necessarily admit a definable satisfaction class, and we cannot in general speak of the theory of a proper class model in ZFC. For real-closed fields, it works because the theory admits elimination of quantifiers, but for the general case we would need to restrict to a theory $T$ for which we could expect a satisfaction class.