Categorical Brouwer-Heyting-Kolmogorov interpretation - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-22T03:05:48Z http://mathoverflow.net/feeds/question/82231 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/82231/categorical-brouwer-heyting-kolmogorov-interpretation Categorical Brouwer-Heyting-Kolmogorov interpretation Zhen Lin 2011-11-29T23:36:27Z 2011-12-15T20:58:51Z <p>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 <em>at most</em> one arrow between any two objects.</p> <p><strong>Question.</strong> 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,</p> <ul> <li>Objects should be propositions.</li> <li>Arrows should be (equivalence classes) of proofs.</li> <li>The coproduct should be disjoint, at least for the coproduct of two distinct atomic propositions.</li> <li>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$).</li> </ul> <p>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.</p> http://mathoverflow.net/questions/82231/categorical-brouwer-heyting-kolmogorov-interpretation/82233#82233 Answer by Finn Lawler for Categorical Brouwer-Heyting-Kolmogorov interpretation Finn Lawler 2011-11-30T00:41:24Z 2011-11-30T00:41:24Z <p>I don't have it with me, and I can't recall the exact details, but I'm pretty sure Lambek &amp; Scott's <em>Introduction to Higher-Order Categorical Logic</em> (<a href="http://books.google.com/books?id=6PY_emBeGjUC&amp;lpg=PP1&amp;pg=PR5#v=onepage&amp;q&amp;f=false" rel="nofollow">link</a>) 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!).</p> http://mathoverflow.net/questions/82231/categorical-brouwer-heyting-kolmogorov-interpretation/83561#83561 Answer by kow for Categorical Brouwer-Heyting-Kolmogorov interpretation kow 2011-12-15T20:58:51Z 2011-12-15T20:58:51Z <p>Perhaps this paper would be good to look at:</p> <p>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 </p>