# Relative consistency of ETCS over the theory of a well-pointed topos with NNO

Gödel's well-known proof of the implication $Con(ZF) \Rightarrow Con(ZFC)$ used the construction of the inner model $L$ in $ZF$ to get a model of $ZFC$ (and in fact much more). However such a construction is not (immediately) available in a category-theoretic approach to set theory. In particular, given a well-pointed topos with NNO, which is the set theory ETCS minus the axiom of choice, I wonder whether there is any way to construct a model of ETCS. On the face of it, it doesn't seem likely, as objects of the given topos are quite amorphous.

The only thing I can think of (admittedly I haven't tried very hard) is by passing to a model of ZF via pure sets, constructing $L$, and then taking the category of sets of $L$. But this is somewhat unsatisfactory, as it leaves the comfy realm of categories and heads out into material set theory. So:

Is there a category-theoretic construction of a model of ETCS from a well-pointed topos with NNO?

-
You could try adding a generic section to every epimorphism. The site's objects would consist of triples $(p,e,s)$ where $p:A \to B$ is epimorphism, $e:B_0 \to B$ is mono, and $s:B_0\to A$ is such that $ps = e$; and the morphisms $(p,e,s) \to (q,f,t)$ are such that $p$ is a restriction of $q$ and $t$ is an extension of $s$ in the only sensible fashion. (Details are too much for a comment box.) Caveat: this is a large site and it's not clear that it will work in only one shot. –  François G. Dorais Jan 3 '13 at 3:11
All these are nice (potential) answers, why not use the answer box? :) –  David Roberts Jan 3 '13 at 4:29
François's idea is very interesting, but the analogue of it for ZF does not work, since one cannot always force ZFC over a ZF model. Although one can force to make any given set well-orderable, simply by making it countable, for example, nevertheless one can have a model of ZF in which every uncountable cardinal is singular, and such a model has no forcing extension satisfying ZFC. –  Joel David Hamkins Jan 3 '13 at 13:34
The $L$ approach also seems to need replacement. Given a wellordering $\alpha$, we can make sense of "the pure transitive set $X$ is $L_\alpha$," we can show that any two such pure transitive sets must be isomorphic and we even have the condensation lemma. If $L_\alpha$ exists for each wellordering $\alpha$, then we can make sense of "the constructible subcategory" by allowing only sets and morphisms that are materializable in some $L_\alpha$. However, replacement is needed to show that there is an $L_\alpha$ for every wellordering $\alpha$ and then that exponentials materialize. –  François G. Dorais Jan 3 '13 at 14:34
@Martin: A proof along the lines suggested in the comments here would not give a new perspective, since it would just be a translation into category theory of an existing set-theoretic proof. But there might well be a category-theoretic proof along entirely different lines that does give a new perspective. (The analogous possibility for the consistency of $\neg AC$ was realized by Freyd's topos-theoretic proof, which is genuinely different from previous forcing proofs, though it could, after the fact, be recast as a forcing argument.) –  Andreas Blass Jan 3 '13 at 21:50
show 16 more comments