Hostname: page-component-7b7567c8c-fvjsw Total loading time: 0 Render date: 2026-11-15T15:28:58.803Z Has data issue: false hasContentIssue false

A categorical version of the Brouwer–Heyting–Kolmogorov interpretation

Published online by Cambridge University Press:  03 February 2004

ERIK PALMGREN
Affiliation:
Department of Mathematics, Uppsala University, PO Box 480, SE-751 06 Uppsala, Sweden Email: palmgren@math.uu.se
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

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.

Information

Type
Paper
Copyright
2004 Cambridge University Press