1
$\begingroup$

Is there a standard reference for understanding sentential, first and higher order logics from a categorical perspective?

I'm close to knowing enough $1$/$2$/internal category theory to tackle the Joyal-Tierney Galois theorem for toposes and the Borceux-Janelidze generalization for internal precategories to give some idea of my knowledge base. I've heard that category theory can model all of these logics as the internal logic of an appropriate (possibly higher) category, and I was looking for a reference that builds up logic from this perspective for someone who has never explicitly read a logic textbook.

For the record I have "A Course in Mathematical Logic" by Bell and Machover ordered and in the mail; I fully intend to take the classical route up through logic as well, but I was curious about any categorical cheat codes along the way.

It seems (naively) like type theory might be the answer here, and I would be open to suggestions in that direction, but I am currently unfamiliar with the inner workings (or general moral) of type theory.

Improve this question
$\endgroup$
5
  • 2
    $\begingroup$ I thought sentential calculus and propositional calculus were synonymous. For that, just good old Heyting algebras would do for a start (Boolean algebras for the classical case). Most traditional treatments will cover classical but not intuitionistic logic; I don't know the text by Bell and Machover, which might be different. $\endgroup$
    – Todd Trimble
    Commented May 28, 2019 at 0:03
  • $\begingroup$ @ToddTrimble Yes, thanks for catching the typo -- I meant to write predicate logic, but there can apparently be first order and higher order predicate logics so I've simply omitted this from the title/question. Awodey's book has a section on Heyting algebras I'll take a look at, thanks for the recommendation. $\endgroup$
    – Alec Rhea
    Commented May 28, 2019 at 0:08
  • 2
    $\begingroup$ The Handbook of Mathematical Logic has a chapter "Doctrines in categorical logic" by Anders Kock and Gonzalo Reyes that, if I remember correctly, does some of what you want. (It dates from 1977,but these logics haven't changed much recently.) $\endgroup$
    – Andreas Blass
    Commented May 28, 2019 at 1:32
  • $\begingroup$ @AndreasBlass Much appreciated, I'll take a look. $\endgroup$
    – Alec Rhea
    Commented May 28, 2019 at 2:43
  • $\begingroup$ For any future readers, in addition to the above references there is a book by Lambek and Scott that appears to be about this topic (github.com/Mzk-Levi/texts/blob/master/…). $\endgroup$
    – Alec Rhea
    Commented May 29, 2019 at 0:17

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .