Finitely Presented Heyting Algebras

Carsten Butz

November 1998

Abstract:

In this paper we study the structure of finitely presented Heyting algebras. Using algebraic techniques (as opposed to techniques from proof-theory) we show that every such Heyting algebra is in fact co-Heyting, improving on a result of Ghilardi who showed that Heyting algebras free on a finite set of generators are co-Heyting. Along the way we give a new and simple proof of the finite model property.

Our main technical tool is a representation of finitely presented Heyting algebras in terms of a colimit of finite distributive lattices. As applications we construct explicitly the minimal join-irreducible elements (the atoms) and the maximal join-irreducible elements of a finitely presented Heyting algebras in terms of a given presentation. This gives as well a new proof of the disjunction property for intuitionistic propositional logic

Available as PostScript, PDF, DVI.

Last modified: 2003-06-08 by webmaster.