Skip to main content
Became Hot Network Question
clarified the wellfoundedness schema.
Source Link

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.

EDIT: As pointed out in comments, the wellfoundedness schema ranging over classes is equivalent to the single statement ranging over sets. Each class can be partitioned into sets via rank, a minimum can be found in each rank, and the resulting transfinite sequence cannot descend infinitely (the image of an $\omega$-sequence without minimum is a set without minimum), so it converges discretely to a true minimum.


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.

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.

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.

EDIT: As pointed out in comments, the wellfoundedness schema ranging over classes is equivalent to the single statement ranging over sets. Each class can be partitioned into sets via rank, a minimum can be found in each rank, and the resulting transfinite sequence cannot descend infinitely (the image of an $\omega$-sequence without minimum is a set without minimum), so it converges discretely to a true minimum.


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.

deleted 45 characters in body
Source Link

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'm working onI've posted a proof of this modified question, and will posted it as a partial answer if/when it's finished. However, my main question is what I'm really interested in, so my answer will remain unaccepted.

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'm working on a proof of this modified question, and will posted it as a partial answer if/when it's finished. However, my main question is what I'm really interested in, so my answer will remain unaccepted.

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.

added 93 characters in body
Source Link

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. SoIn each case, my question is the followingReplacement and Specification schemata are extended as expected, to include formulae with the new symbol.

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?


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'm working on a proof of this modified question, and will posted it as a partial answer if/when it's finished. However, my main question is what I'm really interested in, so my answer will remain unaccepted.

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. 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. So, my question is the following.

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?


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'm working on a proof of this modified question, and will posted it as a partial answer if/when it's finished. However, my main question is what I'm really interested in, so my answer will remain unaccepted.

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'm working on a proof of this modified question, and will posted it as a partial answer if/when it's finished. However, my main question is what I'm really interested in, so my answer will remain unaccepted.

Source Link
Loading