# Reference request about “internal language of categories”

For the last months I've been trying to become familiar with the so-called "internal language of a category". However, I'm still not confident enough when, for instance, I find a subobject (of a given object) which is defined through a formula of the internal laguage of the category I'm considering.

In detail, if $$\mathcal{C}$$ is a pretopos, $$A$$ is an object of $$\mathcal{C}$$ and $$\phi$$ is a formula in the internal language of $$\mathcal{C}$$, I'm not fully able to understand the following two things:

$$1)$$ Which is the actual subobject $$B$$ of $$A$$ represented by the expression $$\{x \in A:\phi(x)\}$$. Meaning, how I can recover $$B$$ in terms of "categorical operations" in $$\mathcal{C}$$.

$$2)$$ How I can work with $$\{x \in A:\phi(x) \}$$. That is, for instance, how I can verify through a completely syntactical procedure that $$\{x \in A:\phi(x) \}$$ is the object I was looking for.

Of course, I'm not asking you to answer points $$(1)$$ and $$(2)$$, as they are too generic. I would prefer if you suggested me a self-contained chapter of a book or some lecture notes where this subject is fully explained. In my opinion, I would especially need a collection of basic examples and exercises regarding its use.

• How comfortable are you with doing this in the usual set-theoretic case, i.e. normal model theory? – Derek Elkins left SE Jun 14 '19 at 20:07
• In that situation I'm comfortable enough, as $\{x \in A : \phi(x) \}$ in this case becomes very natural. I'm familiar with Tarski's definition of semantics, so I know how is defined an $L$-structure for a first order language $L$, if I understood properly your question. – Gennaro Pasquale Jun 14 '19 at 20:19
• You might take a look at the chapter "Doctrines in categorical logic" by Anders Kock and Gonzalo Reyes in the Handbook of Mathematical Logic. – Andreas Blass Jul 11 '19 at 1:47

The answer is, to some extent, there's nothing to do. If you start with a theory, then you just have a bunch of syntactical formulas and subobjects aren't involved until you provide an interpretation. Once you do, a formula $$\varphi(x)$$ where $$x$$ is of sort $$A$$ will simply be interpreted as a subobject of the interpretation of the sort $$A$$. This is a direct generalization of the set-theoretic case.