Skip to main content



Elementary Topos Theory and Intuitionistic Logic

C.L. Mahany

Presented by Andrew K. Hirsch on March 17, 2017

A topos is a particular kind of category whose definition has rich and striking consequences in various contexts. In this expository paper, the role that topoi play in intuitionistic logic is explored through Heyting algebras. In particular, I examine first the relationship between the axioms of intuitionistic propositional calculus and the structure of a Heyting algebra, and then the relationship between the structure of a Heyting algebra and that of a topos. In the third section I derive propositions necessary for the main result. The main result is the proof of the existence of a natural, internal Heyting algebra in any topos.

PDF