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?
Best Answer
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.