# Existence of internal toposes/inner models in a topos

It has been known for some time that one can define a topos as a model of a (finitary) essentially algebraic theory (or in other words, can be defined internal to any category with finite limits). In particular, given a topos $E$ (for instance the topos of sets) one can define an internal topos in $E$ (e.g. a small topos). One can ask for stronger (and in fact is easier to define) in an internal universe: this is a category theoretic analogue of a Grothendieck universe. Such a thing gives rise to an internal topos $M$ in $E$ that is in addition a locally full subcategory. The nontechnical definition is that there is an $E$-object $e(x)$ of $M$-elements of any $M$-object $x$ (recall that elements are functions $1 \to x$, here taken in $M$), and (the $E$-object of) functions in $E$ between $e(x)$ and $e(y)$ correspond to the $E$-object of functions in $M$ between $x$ and $y$.

There are toposes, given a metatheory of $ZFC$, that have no universes in this sense, namely the topos of sets in $V_{\omega+\omega}$, much like one cannot prove the existence of Grothendieck universes in vanilla ZFC.

What I'm curious about is the existence of internal toposes that aren't locally full (equivalently, arise from universes). Shouldn't we get the free internal topos in a topos? If we have NNOs, can we get the free internal topos with NNO? Are there good descriptions of these?

Given the topos of ZFC sets, the models of ZC give internal toposes, but I'm interesting in when we can say something about internal toposes without any material meta-theory. In essence: what can be said about "inner models" in topos theory? When we build inner models in ZFC (say), we leverage the extra structure that material sets have, for instance the cumulative hierarchy, which is not a priori available to the topos theorist.

Postscript: Joyal defined (in work decades old by not yet published) a special sort of category called an arithmetic universe, which is much weaker than a topos, yet has enough structure to define the free internal arithmetic universe in it. I guess the free internal topos should be exist in a topos, but otherwise I can't be sure it's possible. I worry about erroneously "proving the existence of a model" out of nothing.

• An (elementary) boolean topos with nno is certainly able to construct the initial model of an essentially algebraic theory. Note that this model may be degenerate (equal to the terminal model) even if this is not true for the same theory in the real world. Booleanness shouldn't be that essential. Some parts of the classical theory rely on symbols of languages being distinguishable from each other but I don't think that's essential in this case. – François G. Dorais Dec 15 '14 at 8:36
• David, what do you mean by "arithmetic universe" defined by Joyal? And what is your definition of an "internal topos"? Are your definitions of arithmetic universe and internal topos the same as given by John Benabou (and later described in "Problemes dans les topos")? – Michal R. Przybylek Dec 15 '14 at 12:59
• @Michal Joyal's definition has never been published or even circulated, so I can only point to work of Maietti (published in Theory and Appl. of Categories) and Paul (see link in his answer below). An internal topos is a model of the finite limit theory of toposes (I take the axioms to be pullbacks, Cartesian closed, subobject classifier, NNO, all given by specified operations). This is probably the same as what is in Problemes dans les topos, I don't have it in front of me. – David Roberts Dec 15 '14 at 22:35
• Thanks, David, I'll take a look into the paper. But, anyway, I think it was Jean Benabou who first introduced the notion of an internal topos (BTW: I meant JEAN Benabou, of course. I can't believe I've written John. Shame on me...) – Michal R. Przybylek Dec 15 '14 at 22:41
• @Michal fair enough, I know the history of these ideas is convoluted... – David Roberts Dec 16 '14 at 4:03

Your long question suggested at first that you were asking for something difficult (a locally full internal topos), but you ended up asking for the easy thing.

Starting from your postscript, the purpose of an arithmetic universe is that it is is the least categorical structure in which one can construct the free or initial structure of a widely applicable kind, namely essentially algebraic. (See my answer here for a brief explanation of arithmetic universes.) Any elementary topos with natural numbers object is an arithmetic universe.

The structure of an elementary topos (with natural numbers if you wish) is essentially algebraic, so

There is an initial elementary topos with natural numbers in any arithmetic universe, in particular in any elementary topos with natural numbers.

I would like to refer you to the books 2-Categories for the Working Categorist and Introduction to Arithmetic Universes, but regrettably nobody has written them yet.

Talking about ZFC or cumulative hierarchies in this is really obfuscation. However, I indicated how to build the set-theoretic hierarchy in my paper Intuitionistic Sets and Ordinals, based on earlier ideas of Gerhard Osius.

As François Dorais points out above, the initial model may be degenerate, just as it may be in any situation in logic or algebra, and so much more difficult questions of consistency or incompleteness arise. Indeed, André Joyal proved Gödel's incompleteness theorem categorically in the following form:

In the initial arithmetic universe $\mathcal A$, the internal hom-object $A(1,0)$ of its internal initial arithmetic universe $A$ (where $0,1:{\mathbf 1}\rightrightarrows A$ are the internal initial and terminal objects of $A$) is not isomorphic to the initial object $\mathbf 0$ of $\mathcal A$.

On the other hand, again as in traditional logic, if the outer structure is of a stronger kind than the inner one then there are methods of proving internal consistency.

For example, the natural numbers provide a bare-hands model of set theory (without inifinity), in which $n\epsilon m$ if the $n$th binary digit of $m$ is $1$, and so a Boolean internal elementary topos.

A particularly neat and powerful method is the gluing construction (known in computer science as logical relations); for my account of this see Section 7.7 of my book.

• Thanks, Paul. I learned of the arithmetic universe stuff from your answer here on MO, then following references. I guess I wanted reassurance on the internal free topos, but I'm really mystified by what should be analogues of inner models. The best I can think of is to have a topos fibred over a base topos that is the externalisation of an internal topos, and arising from some syntactic construction. – David Roberts Dec 15 '14 at 9:03
• Ah, that's what I was worried about, incompleteness phenomena. Thanks also for explaining what Joyal actually proved, in my limited reading around on the issue I'd not seen it written down. – David Roberts Dec 15 '14 at 22:38