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

EDIT: I'm bumping this, because I'm still curious, and because I have a relative consistency result over the theory of a well-pointed topos with NNO, and I am wondering how much baggage I save by not assuming AC in the base model (I'm not using AC in the proof either).

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?

• Naïvely one might just take the full subcategory of the topos with NNO spanned by the well-orderable objects... but there's no guarantee that this subcategory is closed under power objects, so this probably doesn't work. But maybe a non-full subcategory will do the trick. – Zhen Lin Jan 3 '13 at 2:12
• 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
• 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

I confess that I am not altogether clear what the Question requires, whilst many of the Comments are beyond me, but here is a construction of which you may not be aware and which may throw some light on the issues.

It is based on my paper Intuitionistic Sets and Ordinals, in the Journal of Symbolic Logic 61 (1996) 705-744, particularly Section 3. This in turn built on Categorical Set Theory: a characterisation of the Category of Sets by Gerhard Osius in the Journal of Pure and Applied Algebra 4 (1974) 79-119.

We are working in some given elementary topos, whose objects I will call carriers in order to avoid the word set.

A model of a fragment of set theory is given by a carrier $X$ equipped with a binary relation $\epsilon$ that it is convenient to regard as a map $\epsilon:X\to P X$ to the powerset. That is, it is a coalgebra for the covariant powerset functor.

We say that $(X,\epsilon)$ is extensional if the map $\epsilon:X\to P X$ is mono (1-1).

The definition of when the coalgebra is well founded involves a pullback diagram and is given in the paper.

Then an ensemble is an extensional well founded coalgebra.

Applying the covariant powerset functor to one ensemble gives another.

Between any two ensembles there is at most one coalgebra homomorphism, and it is mono. This captures inclusion in the set-theoretic sense.

The category of ensembles is therefore a preorder. It is a large category in the same sense that familiar categories such as that of groups in a topos are large.

We can rehearse the standard definitions of pairing, functions, etc from set theory using ensembles and show that this preorder provides a model of the Zermelo axioms.

Natural numbers (infinity) and the axiom of choice are inherited from the given topos if it has them.

As to the axiom-scheme of replacement, understanding this from a categorical perspective was one of my principal aims in this work. The comments in my JSL paper are really quite naive and should be discounted in favour of those at the very end of my book, However, I got interested in other things and never pursued this to a satisfactory conclusion.

• Hi Paul, thanks for pointing out your paper, but my question was asking for a way to construct a model of ETCS (i.e. with AC) from a well-pointed topos with NNO (i.e. no AC assumed), without passing through Zermelo(-Fraenkel) set theory. – David Roberts Feb 6 '15 at 1:08
• @David, I have just tried to send you an email in Adelaide but it was bounced with a 554 error. – Paul Taylor Feb 6 '15 at 11:47
• Try droberts.[largest known Fermat prime]@gmail.com – David Roberts Feb 6 '15 at 20:04