Categorical Brouwer-Heyting-Kolmogorov interpretation - MathOverflow

Categorical Brouwer-Heyting-Kolmogorov interpretation

2011-11-29T23:36:27Z

Let $\mathcal{L}$ be the language of intuitionistic propositional logic generated by some atomic propositions $t_1, t_2, \ldots$. The Lindenbaum–Tarski algebra of $\mathcal{L}$ can be regarded as a bicartesian closed category in which there is an arrow $p \to q$ if and only if there is a proof of $q$ assuming $p$. Unfortunately it is a somewhat dull category, as there is at most one arrow between any two objects.

Question. Is there a categorification of the Lindenbaum–Tarski algebra which enables a category-theoretic form of the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic propositional logic? In particular,

Objects should be propositions.
Arrows should be (equivalence classes) of proofs.
The coproduct should be disjoint, at least for the coproduct of two distinct atomic propositions.
The terminal object should be indecomposable, so that the disjunction property is validated (i.e. an arrow $\top \to p \lor q$ is either an arrow $\top \to p$ or an arrow $\top \to q$).

It feels like the free bicartesian closed category generated by the atomic propositions is the most likely candidate, and it can be concretised by the Yoneda embedding into the presheaf topos: then we would have a genuine BHK interpretation, i.e. interpreting a proposition as the ‘set’ of its proofs. This has probably been well-studied, in which case I would appreciate any references to the literature.

Answer by Finn Lawler for Categorical Brouwer-Heyting-Kolmogorov interpretation

2011-11-30T00:41:24Z

I don't have it with me, and I can't recall the exact details, but I'm pretty sure Lambek & Scott's Introduction to Higher-Order Categorical Logic (link) is what you're looking for. In particular, they prove the equivalence between cartesian closed categories and simply-typed $\lambda$-calculi (so you get the Curry--Howard correspondence for free!).

Answer by kow for Categorical Brouwer-Heyting-Kolmogorov interpretation

2011-12-15T20:58:51Z

Perhaps this paper would be good to look at:

ERIK PALMGREN (2004). A categorical version of the Brouwer–Heyting–Kolmogorov interpretation. Mathematical Structures in Computer Science, 14 , pp 57-72 doi:10.1017/S0960129503003955