10
$\begingroup$

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).

Improve this question
$\endgroup$
5
  • $\begingroup$ First of all is it clear to you how to do it in a topos? $\endgroup$
    – fosco
    Commented Jun 15, 2019 at 7:55
  • $\begingroup$ No, unfortunately it isn't. $\endgroup$
    – Matteo Spadetto
    Commented Jun 15, 2019 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
    Commented Jun 15, 2019 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
    Commented Jun 15, 2019 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
    Commented Sep 25, 2019 at 13:39

1 Answer 1

Reset to default
2
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .