I was recently introduced to the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic, and since I am just starting out with basic category theory and have heard that topos logic is intuitionistic, I wondered if there is a natural way to turn this interpretation into a category.

Basically, and I am going off pure intuition here, I want the objects to be formulas and the morphisms to be functions from a proof of $P$ to a proof of $Q$. In this way it seems that $P\wedge Q \simeq P\times Q$ (the product), because there are projection arrows from $P\wedge Q$ to $P$ and to $Q$; also, if anything else projects to $P$ and $Q$ we may deduce $P\wedge Q$ from it. In a similar manner $P\vee Q \simeq P+Q$ (the co-product), if my interpretation is correct. Moreover, the formula $(P\rightarrow Q)$ (the arrow here is a deduction arrow and not a morphism) seems to me to be the colimit of the diagram $\require{AMScd}$ \begin{CD} P @>f>> Q \end{CD}

This is a bit confusing and tautological, as we are using arrows in two distinct, but similar ways (exactly because this is the BHK interpretation of logical deduction). Now, the tautologies (i.e. $(P\rightarrow P)$) should function as terminal objects, all isomorphic to each other. If we denote by $\bot$ the so-called "absurdity", then it should serve as an initial object, because everything can be deduced from it. So now $\lnot P$ can be defined as the colimit of $\require{AMScd}$ \begin{CD} P @>>> \bot \end{CD} This is where my definitions fall apart, because it is said that the absurdity should have no proofs, so we cannot really form the negation of a formula using the colimit definition from before.

I am doing this mostly as an exercise to test my understanding of basic category theory concepts, so I have two questions: is there a way to turn this into a formal category and if yes, is it possible to extend to first-order logic in it?

  • $\begingroup$ You don't want a colimit for implication, you want an exponential object. Then $P\to \bot$ makes perfect sense with $\bot$ an initial object. $\endgroup$ – Malice Vidrine Oct 19 '19 at 16:56

One of the semantics for intuitionistic propositional logic is to interpret propositions' "truth values" in a Heyting algebra instead of a Boolean algebra. One of the ways to define a Heyting algebra is as a partial order that, as a thin category, is finitely cocomplete and Cartesian closed. This suggests that we can probably interpret intuitionistic propositional logic more generally in finitely cocomplete Cartesian closed categories, and this does in fact work.

Note that a colimit of a morphism $P\to Q$ is the wrong way to think about an implication. That colimit is going to be isomorphic to $Q$ itself. Rather you want the exponential object $Q^P$ provided by Cartesian closedness; one way to see this is to see that the evaluation map for exponentials, in propositional terms, essentially establishes modus ponens.

There is a way to extend the idea to first order logic, but it takes a little more gear. The easiest setup to understand for the first order case is where we have functor $P:\mathcal{C}^{op}\to\mathbf{Cat}$ such that $P(C)$ is finitely cocomplete and Cartesian closed for all $C$, and the $P(f)$ preserve that structure and all have left and right adjoints satisfying some nice-ness conditions. Then we can think of the objects of $P(C)$ as "predicates on $C$", the $P(f)$ as "substitution of terms", and the right and left adjoints are quantification. There are more general structures that are more flexible than these $\mathbf{Cat}$-valued functors, but I think these are the easiest gateway for later figuring out what those structures (namely fibred categories) are trying to do, should you end up wanting to look into them more.

  • $\begingroup$ great! would you point to some relevant literature on the topic (I know only of Goldblatt's Topoi)? also, is there a name for this specific category? $\endgroup$ – Bogdan Simeonov Oct 19 '19 at 22:11
  • 1
    $\begingroup$ There's not really a specific name for it, but I should have said something about how "giving rise to a category" isn't really the best way to look at it. The question I answered is somewhat of a re-reading: what are we asking of a category when interpreting propositions as its objects? You can also make a Cartesian closed category out of a propositional theory, but I think the considerations above are what tell you why you'd want to. In any case, I think you'd enjoy Introduction to Higher Order categorical Logic by Lambek & Scott. It looks at his in a number of interesting ways. $\endgroup$ – Malice Vidrine Oct 19 '19 at 22:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.