A categorical version of the Brouwer--Heyting--Kolmogorov interpretation Export

@misc{citeulike:401348, abstract = {In this paper we interpret (fragments of) intuitionistic logic in categories with weak closure properties, such as quasi left exact categories and locally cartesian closed categories (LCCC) with sums. We also interpret the full choice scheme in an LCCC. The interpretation can be seen as a categorical form of the usual Brouwer-Heyting-Kolmogorov (BHK) interpretation. The standard interpretation of geometric logic in a pretopos is obtained by applying the image functor to the BHK-interpretation...}, author = {Palmgren, Erik}, citeulike-article-id = {401348}, citeulike-linkout-0 = {http://citeseer.ist.psu.edu/palmgren02categorical.html}, citeulike-linkout-1 = {http://citeseer.lcs.mit.edu/palmgren02categorical.html}, citeulike-linkout-2 = {http://citeseer.ifi.unizh.ch/palmgren02categorical.html}, citeulike-linkout-3 = {http://citeseer.comp.nus.edu.sg/palmgren02categorical.html}, keywords = {cat, categorical, lextensiva, logic}, posted-at = {2005-11-19 16:39:09}, priority = {0}, title = {A categorical version of the Brouwer--Heyting--Kolmogorov interpretation}, url = {http://citeseer.ist.psu.edu/palmgren02categorical.html} }

TY - GEN ID - citeulike:401348 L3 - citeulike-article-id:401348 N2 - In this paper we interpret (fragments of) intuitionistic logic in categories with weak closure properties, such as quasi left exact categories and locally cartesian closed categories (LCCC) with sums. We also interpret the full choice scheme in an LCCC. The interpretation can be seen as a categorical form of the usual Brouwer-Heyting-Kolmogorov (BHK) interpretation. The standard interpretation of geometric logic in a pretopos is obtained by applying the image functor to the BHK-interpretation... TI - A categorical version of the Brouwer--Heyting--Kolmogorov interpretation KW - cat KW - categorical KW - lextensiva KW - logic AU - Palmgren, Erik UR - http://citeseer.ist.psu.edu/palmgren02categorical.html ER -