ABSTRACT

This chapter reviews the system of intuitionistic propositional logic in terms of the sequent calculus. The logical rules determine a notion of algebraic structure that models the logic. All the algebraic concepts needed to model intuitionistic propositional logic are thus standard, except perhaps the one relative to implication. For a topological characterization of finite Heyting algebras, it is convenient to introduce the notion of co-point. On the one hand, this is a strengthening of the notion of atom for Boolean algebras (i.e. of an element different from 0 and with no elements between it and 0), which does not play any significant role for Heyting algebras. On the other hand, this is a paradigm for further generalizations that will play a fundamental role. One extends the notions of Stone space and Stone topology to arbitrary Heyting algebras by considering the set of prime filters and its topology.