Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question
    
Related: mathoverflow.net/questions/43281/… –  Qiaochu Yuan Nov 29 '11 at 23:53
add comment

2 Answers 2

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

share|improve this answer
1  
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. –  Zhen Lin Nov 30 '11 at 7:50
add comment

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

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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