Does the BHK interpretation induce a category?

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?

• 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. – Malice Vidrine Oct 19 '19 at 16:56

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.