Some reference for categorical logic?

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!


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 recommend Goldblatt's Topoi: The Categorical Analysis of Logic. (Have a look at this question of mine.)

This MO question is also relevant.