Is there a universal way to force the Axiom of Choice to be true?

Question

Given a model of set theory $V$ there are various ways to construct a model in which the Axiom of Choice holds, such as Gödel's constructible universe $L^V$ or by using forcing*. I'm wondering if any of these constructions have a nice universal property in the sense of category theory.

In particular are there any adjoints to the inclusion 2-functor $\mathcal{ZFC}\to\mathcal{ZF}$?

(Where $\mathcal{ZF}$ is the 2-category whose objects are either

1. Models of ZF
2. Toposes

and whose morphisms are either

1. Geometric morphisms
2. Logical functors
3. Elementary embeddings**

and where $\mathcal{ZFC}$ is the full subcategory on the objects that obey Choice.)

I think that the concept of the "minimal model" might allow one to construct a right adjoint which is similar in character to the constructable universe. Forcing goes "the other way" by adding sets rather than restricting them, so I suspect it might give a left adjoint.

*Or not? See comments.

**Asaf Karagila notes that there can't exist an elementary embedding between a model where Choice holds and one where it doesn't. So there can't be an adjunction in this case, because its unit or counit would sometimes have to be such a morphism. But perhaps there's some other kind of morphism between models of ZF that does allow an adjunction?

Answer 1

Too long to be a comment but not really answer either. This is an interesting question because it is phrased in terms of category theory. There are various way of forcing the full axiom of choice over models of $ZF$ which already satisfy weak forms of choice.

For example starting with $L(\mathbb{R})$ and assuming $AD+DC$, one may force the full axiom of choice using $\mathbb{P}_{max}$ forcing. This forcing will add a wellordering of the reals of length $\aleph_2$ and thus achieve $\Theta=\aleph_3$ ($\Theta$ is the sup of the length of the prewellordering of the reals, useful in non-$AC$ context). The wellordering of the real is not added in the usual way, using say $Coll(\omega_1,<\mathbb{R})$. The reason behind forcing $AC$ here traces back to the existence of stationary-co-stationary subsets of $\omega_1$. In fact, if there exists a stationary-co-stationary subset of $\omega_1$ then there is an $\omega_1$-sequence of distinct reals (this is already a manifestation of a weak form of choice if the elements of the model are all ordinal definable from reals)

The above technique is not general enough because forcing choice will disturb the cardinal arithmetic of the model in general. We believe we have proved recently that if one starts with $AD+DC$ in $L(\mathbb{R})$ then one may force $AC$ while making the continuum $\aleph_3$. This is very different from $\mathbb{P}_{max}$ forcing but it is still entirely possible that there is some deep structure which accounts for very general methods on how to force choice, under large cardinal hypothesis. Forcing various degrees of generalizations of $DC$ is crucial to achieve the result.

I would be very interested to see how this translates into a category theoretic framework and see if there is a way to gauge the "universality" of the method.

As mentionned by Joel, starting from $ZF+DC$ one may force $AC$ using $Coll(\omega,<\mathbb{R}).$ By forcing theory this wellorders the reals, does not add reals and one obtains $CH$ from it.

Finally, in a different direction, David Pincus has shown how to transform a model of a statement $\phi$ into model of $\phi+DC$, see the following article: Adding Dependent Choice. The contents of the article seem to be more amenable to a category theoretic approach than the results we've mentioned above.

Answer 2

Following up on my remarks in the comments, allow me to answer from the perspective of model-theoretic interpretations of theories. I view interpretations of theories as providing particularly strong forms of the desired functors between these categories.

Specifically, an interpretation of one theory $S$ in another theory $T$, is a uniform way of defining a model of $S$ inside any model of $T$. Given a model of the latter theory $M\models T$, one defines a domain $N$ and functions and relations on this domain, such that with this structure it becomes a model of the first theory $N\models S$.

Two theories are mutually interpretable, if each of them is interpreted in the other. So in any model of the one theory $M\models T$ you can define model of the other theory $N\models S$, and inside $N$ you can define a model $\bar M\models T$ of the first theory again.

The thing to notice is that with mutual interpretability, there is no insistence that these interpretations are inverse of each other, and it could be that $M$ and $\bar M$ are not much related. Perhaps this makes them rather un-adjoint-like.

A much stronger notion, therefore, imposes the uniform inverse requirement. Specifically, theories $S$ and $T$ are bi-interpretable if they are mutually interpretable in such a way that the interpreted model $\bar M$ arising in $N$ is isomorphic to $M$ and furthermore, isomorphic by an isomorphism that is definable in $M$, and vice versa in the other direction.

The relevance of this for your question is that ZF and ZFC are not bi-interpretable.

Theorem. Distinct extensions of ZF are never bi-interpretable.

Thus, one cannot transform ZF models and ZFC models into one another in such a way that they form a bi-interpretation, and I take this to be a kind of negative answer to a strong version of the question.

I recently made a blog post providing a proof and further discussion of this theorem and related matters:

Different set theories are never bi-interpretable.

(The theorem follows from results of Albert Visser in his 2006 paper, "Categories of theories and interpretations." In addition, there is a nice automorphism group model-theoretic argument of Ali Enayat showing for the specific case of ZF and ZFC that they are not bi-interpretable. Follow the link at my blog.)