I've tried to become familiar with the so-called "internal language of a category" for the last months. 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 that I'm considering.

In detail, if $C$ is a pretopos, $A$ is an object of $C$ and $\phi$ is a formula in the internal language of $C$, I'm not completely 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 can I recover $B$ in terms of "categorical operations" in $C$?

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

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

Thanks in advance.

P.S. I asked the same question in Math Stack Exchange (https://math.stackexchange.com/questions/3262479/reference-request-about-internal-language-of-categories).

  • $\begingroup$ First of all is it clear to you how to do it in a topos? $\endgroup$ – fosco Jun 15 '19 at 7:55
  • $\begingroup$ No, unfortunately it isn't. $\endgroup$ – Gennaro Pasquale Jun 15 '19 at 9:34
  • $\begingroup$ Welcome to MO, Gennaro! I'm not sure I understand the question. Are you familiar that the internal $\wedge$ corresponds to intersection of subobjects, that the internal $\vee$ corresponds to join of subobjects and so on? $\endgroup$ – Ingo Blechschmidt Jun 15 '19 at 20:19
  • 4
    $\begingroup$ Don't worry, we all begin from not knowing it; but you'll like it, and you'll never forget it! Look into Mac Lane's-Moerdijk Sheaves in Geometry and Logic, from page 296 on. $\endgroup$ – fosco Jun 15 '19 at 20:42
  • 3
    $\begingroup$ Very often when using internal logic we do not know what is the exact translation of all the statement we write. We have an explicit procedure that turn any explicitly written statement in a sub-object, but as soon as the formula is a little complicated, explicit writing the translationis painful. To me the point of internal logic is to not do the translation, or more precisely to only do it when it is easy. Ideally you'll use internal reasoning to show a connection between two formula that are easy to translate, using intermediate thing that you do not want to translate. $\endgroup$ – Simon Henry Sep 25 '19 at 13:39

Here are some resources:

  1. Carsten Butz.Regular categories and regular logic, notes, 1998.
  2. P. Freyd and A. Scedrov. Categories, Allegories. North–Holland, Amsterdam 1990.
  3. S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic. Springer–Verlag, New York 1992.
  4. B. Jacobs, Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, North Holland, Elsevier, 1999.

The first one covers the fragment of logic with $\top$, $\land$, $\exists$ and $=$. The second one has first-order categorical logic, and the third one higher-order logic. Jacobs's book is very thick and intimidating, I am mentioning it because it contains rules for $\lbrace x : A \mid \phi(x)\rbrace$, which you're asking about.


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.