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.

Thanks in advance.

  • $\begingroup$ How comfortable are you with doing this in the usual set-theoretic case, i.e. normal model theory? $\endgroup$ – Derek Elkins left SE Jun 14 '19 at 20:07
  • $\begingroup$ 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. $\endgroup$ – Gennaro Pasquale Jun 14 '19 at 20:19
  • $\begingroup$ You might take a look at the chapter "Doctrines in categorical logic" by Anders Kock and Gonzalo Reyes in the Handbook of Mathematical Logic. $\endgroup$ – 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.

If you start with a pretopos, then the internal language of that pretopos will simply have a predicate symbol for each subobject. Of course, we'll have an interpretation that will interpret each such predicate symbol as the subobject it corresponds to. This is more or less the counit of this adjunction. This procedure may lead to a theory that has a proper class of predicate symbols and axioms, and I believe you just have to stretch your notion of theory to accept that.

Now to be clear, it is important to separate a subobject from a monomorphism. A subobject is an equivalence class of monomorphism. Having a subobject doesn't provide you with a particular object. You may need the Axiom of Global Choice to pick representatives if no other structure is available. (Maybe there's a way to get away with less in general, perhaps using Scott's trick.)

To prove things, you just prove things like normal in the theory. For the theory generated from the given pretopos, you'll have an axiom asserting every formula that you can formulate in the theory with predicate symbols corresponding to subobjects which is true under interpretation. In other words, for the theory generated from the given pretopos, a formula is provable if and only if its interpretation is true in the given pretopos.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.