I’ve been really having a hard time trying to understand categorical semantics. In fact, I am confused to the point I am afraid I don't know how to ask this question!
I’ve been reading textbooks like Makkai and Reyes’ book, Jacobs’ Categorical logic and type theory (1992) or Categorical Logic by Andrew Pitts, but I simply cannot get the feeling of what are they trying to do. This entry and this one in the nlab do not seem to be very helpful for my understanding. In fact, it seems that the more I read the more confused I get.
Can those questions be answered crystal clearly?
-
How we define a categorical interpretation?
-
If it a functor, what is its domain? That is, in model theory, we interpret languages. What are we interpreting here, languages or theories .. or something else?
Let me take an example: I know, very informally, that intuitionistic propositional logic (IPL) correspond to bicartesian closed categories (BCC).
- But how to make this statement mathematically precise?
How do we define such an interpretation?
If it is indeed a functor, what is its domain? The category of intuitionistic propositional logics or the category of intuitionistic propositional languages? Or even a particular intuitionistic propositional logic understood as a categry (possibly given by the category of proofs)?
I would really appreciate any answer that could shed some light not only into this example, but also into the big picture of it.
Background: I believe to have all the required background in category theory (UPs, natural transformations, equivalences, adjoints etc.) and type theory (polymorphism, dependent types etc.), having attended courses in both disciplines.
Best Answer
There are (at least) two different sort of things you can do, roughly corresponding to syntax and semantics.
You can study the internal logic of a category, which lets you use a logical language as a convenient tool for doing calculations with in a category. e.g. objects are types, propositions are subobjects, et cetera.
Conversely, given a suitable language, we can construct its syntactic category consisting of all the types you can construct in the language and the functions you can define between them, and satisfying all of the relations you can prove hold between them. And thus we can use category theory to help us think of type theories.
On the semantic side we can think of a category $T$ (possibly with extra structure; e.g. a sketch) as being a theory. Then models of this theory in a category $C$ will be functors $F : T \to C$ of a certain type.
Of course, these aren't unrelated; if we have the theory of a group, we might then construct $T$ to be its syntactic category, and require the functors defining models of $T$ to be of the sort that preserves the logic used.
Conversely, if we're in the habit of studying functors out of some category $T$, it may be worth considering the theory given by internal language of $T$ and view functors as being models of that theory.
A common type of this construction is one we can do with universal algebra (e.g. the theory of groups, given as operations and equations). If we have some variety of universal algebra, we can take $T$ to be the opposite category of the category of finitely presented algebras, and then models will be functors from $T$ that preserve finite limits.