8
$\begingroup$

There seem to be many version of the notion "the internal language of a category", with which I'm kinda confused.

For example, in any standard textbooks on topos theory, we have the notion of internal language of a topos, which is a logic.

There is also the internal language of a cartesian closed category, which is a type theory (e.g. in Awodey's draft, 4.6). Where basic types are objects, morphisms become functions, with some axioms.

In nLab The internal language (as a type theory) for a locally cartesian closed category is defined to have closed types the objects, and dependent types as morphisms, contexts as tower of morphisms, and terms as sections (which I'm also confused with, a section is a morphism per se, so is should be interpreted as a dependent type already?)

There could be more that I will not enumerate here. My question are:

  1. Is there a very general definition of internal language of an arbitrary category or a very general class of categories, so it unifies all those variant versions?
  2. Is there any relationship when we refer to internal language as logic with when we refer to it as a type theory? (Can they be unified?)
$\endgroup$
4
  • $\begingroup$ An arbitrary category has far too little structure to support an internal language that can say anything interesting. It should be clear from the examples you already know: the internal logic of a topos is rich and expressive because a topos is a very special kind of category. $\endgroup$ Commented 14 hours ago
  • $\begingroup$ @ZhenLin Is there a minimal requirement for categorical structure to support an internal language, or is it just "uninteresting" to consider them but we do have such a notion? $\endgroup$ Commented 12 hours ago
  • $\begingroup$ I don't know what you imagine an internal language to be. To give an extreme example, obviously it is possible to interpret the empty language in any category. $\endgroup$ Commented 12 hours ago
  • $\begingroup$ @Westlifer You can get away with as little structure as having finite products, depending on what exactly you want to do. $\endgroup$ Commented 7 hours ago

1 Answer 1

Reset to default
3
$\begingroup$

You should think of structure on a category as being related to expressiveness of its internal logic. I don't personally know of any "uniform" way to guess which categorical structures should be related to which logical features, but I'm sure people have thought about it.

One common approach is to start with a "well known" correspondence between categories and logic (eg: topoi and IHOL, or cartesian closed categories and $\lambda$-calculus) and then perturb one side by adding/removing structure on the categorical side or constructors on the logic side.

So, for example, you can start with the internal logic of topoi -- a type theory with power-objects, dependent sums/products, etc. -- and slowly step down the logical strength to geometric, or coherent, or regular, or lex, or algebraic logic. This allows you to similarly step down the required structure on your category, and the fun and surprising fact is that the categories that arise in this way are independently interesting!

Instead, you might start with the internal logic of cartesian closed categories -- $\lambda$-calculus -- and then change the categorical structure. For instance, you might replace cartesian closed by "symmetric monoidal closed" and you'll recover (intuitionistic multiplicative) linear logic. Then you might want to add the $!$-exponential from linear logic back in, and if you look at what that would mean for the category you'll find yourself considering comonads with certain properties.

You can play this game forever, making small changes to your logic and your category, and it's quite fun to do! I recommend looking at the table here, which shows many of these pairs (many of which come from weakening the internal logic of topoi).

I hope this helps ^_^

$\endgroup$
1
  • 2
    $\begingroup$ Maybe refine to "simply typed $\lambda$-calculus" in the example of cartesian closed categories, to distinguish it from the untyped $\lambda$-calculus that's often considered in CS? $\endgroup$ Commented 4 hours ago

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.