Skip to main content
3 of 4
deleted 45 characters in body

Global Choice bi-interpretable with Global Wellorder?

It's well known and quite trivial that $\sf{ZF}$ with global choice is mutually interpretable with $\sf{ZF}$ plus a global wellordering. However, a much less obvious question is whether the two theories are bi-interpretable. The non-obvious nature of this question is revealed when investigating how exactly the mutual interpretation is conventionally performed.

When interpreting a global wellorder, assuming global choice, typically we apply the wellordering theorem. To be careful, each layer of the cumulative hierarchy is wellordered individually, and then all those wellorders can be concatenated into a global wellorder with the help of a global choice operator. The reverse interpretation is much simpler: given a global wellordering relation, the corresponding "$\min$" operation is immediately a global choice operation. These strategies are well known.

When considering the question of bi-interpretability however, an issue arises: the above mechanisms are not inverses! Composing the two interpretations does not necessarily lead to isomorphism. Indeed, a great many choice functions could lead to the exact same wellorder. Worse still, intuitively the vast majority of global choice functions will fail to agree with the $\min$ function of a wellorder. Similarly, the decision to construct the wellorder by stratifying $V$ via the cumulative hierarchy restricts our strategy to only construct setlike wellorders. In fact, all the wellorders we produce are rank-respecting.

To obtain bi-interpretability between Global Choice and a Global Wellordering, we would require something akin to a definable bijection between global choice functions and global wellorderings. My question is essentially whether this is possible.

If we augment $\sf{ZF}$ with a function symbol implementing Global Choice, is that bi-interpretable with the augmentation of $\sf{ZF}$ by a Global Wellorder relation?

To address the technicalities: the choice function is just a new symbol we add to the signature, and we assert axiomatically that it produces as output a member of the input set, provided the input is nonempty. Similarly the order relation is introduced as a new symbol, asserted to be a total order, and it's asserted to be a wellorder as a schema ranging over definable collections. In each case, the Replacement and Specification schemata are extended as expected, to include formulae with the new symbol.


A slightly easier question is whether we get bi-interpretability by restricting the wellorder to be setlike. I suspect we can get an affirmative answer in that case, but I'm not sure yet. If we further require our wellorder to be rank-respecting, however, then I think I have a proof of bi-interpretation. To be precise, a wellordering relation $<$ is said to be rank-respecting precisely when the following holds, where $\operatorname{rank}(x)$ denotes the ordinal rank of the wellfounded set $x$. $$\operatorname{rank}(x)\subsetneq \operatorname{rank}(y) \implies x<y$$

The modified version of my question, where the wellorder is restricted to be rank-respecting, is stated below.

If we augment $\sf{ZF}$ with a Global Choice operator, is that bi-interpretable with $\sf{ZF}$ augmented by a rank-respecting Global Wellorder relation?

I've posted a proof of this modified question as a partial answer. However, my main question is what I'm really interested in, so my answer will remain unaccepted.