# Some reference for categorical logic?

By "categorical logic" I mean category-theoretical models of logic. In particular, I am more interested in models of intuitionistic predicate logic with conjunction, disjunction, implication and quantifiers.

I know about a book of Lambek and Scott and another one by Makkai and Reyes, but these are quite old, especially the second. Does anyone know any newer books/resources on this topic?

For example, I have studied on propositional intuitionistic logic (with $\bot,\wedge,\vee$ and $\to$) and the corresponding category-theoretical model is a bicartesian closed category (objects are formulas and arrows are proofs). But what is the case with predicate intuitionistic logic? Is there any more recent text analyzing this case?

-

I'm not sure what the most recent texts would be, but most of what you are asking about would probably fall into the general category of topos theory.

Mac Lane and Moerdijk's Sheaves in goeometry and logic (1992) is probably still the best place to start, although if you find it tough going, you could try McLarty's Elementary Categories, Elementary Toposes (1992). If you need a more elementary introduction to category theory, try Awodey's Category Theory (2006) or the texts by Barr and Wells (Category Theory for Computing Science or Triples, Toposes, and Theories), although these aren't as recent.

If you really want to bite off more than you can chew, there is Johnstone's Sketches of an Elephant (2002), but you should almost certainly wait a while before trying to tackle that! Somewhat more accessible, but still more of a reference than a textbook is Johnstone's classic Topos theory (1974), which is now back in print!

-
Thanks a lot! This is a whole bibliography! –  frabala Mar 14 at 22:55

Besides the very good books on topos theory already mentioned, I highly recommend Categorical Logic by Andrew Pitts for an introduction to the categorical semantics of type theories (you can find it online here. See Section 5 for the treatment of predicate logic).

The more advanced Categorical Logic and Type Theory by B. Jacobs, from the series Studies in Logic and the Foundations of Mathematics, is another good reference on the subject.

-
I already checked your first recommendation and it fits quite well for what I needed! Thanks! –  frabala Mar 14 at 22:54

I recommend Goldblatt's Topoi: The Categorical Analysis of Logic. (Have a look at this question of mine.)

This MO question is also relevant.

-
I checked the book. Unfortunately, it's not what I wanted, because it doesn't study predicate logic, but algebraic and topological models of propositional logic only. The MO question, though, is a good link. Thanks! –  frabala Mar 14 at 22:57
It covers predicate logic in the context of first order languages at least at the start of the 11th chapter, but fair enough. You're welcome :) –  Shaun Mar 14 at 23:14