8
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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!).

$\endgroup$
  • 1
    $\begingroup$ In Part I, section 11, Lambek and Scott construct the cartesian closed category generated by a typed λ-calculus, which I can believe is what I want, except on the wrong side of the Curry–Howard isomorphism. It's not clear to me that the terminal object $\top$ is indecomposable in this category though – they only prove the disjunction property in the context of toposes and type theory later in the book, via the Freyd cover. $\endgroup$ – Zhen Lin Nov 30 '11 at 7:50
2
$\begingroup$

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

$\endgroup$

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.