Table of contents

1 Formal definitions 2 Properties 3 Examples 4 References

Formal definitions

A Heyting algebra H is a bounded lattice such that for all a and b in H there is a greatest element x of H such that a ∧ x ≤ b. This element is called the relative pseudo-complement of a with respect to b, and is denoted a⇒b (or a→b).

An equivalent definition can be given by considering the mappings f_a: H→H defined by f_a(x) = a∧x, for some fixed a in H. A bounded lattice H is a Heyting algebra iff all mappings f_a are the lower adjoint of a Galois connection. In this case the respective upper adjoints g_a are given by g_a(x) = a⇒x, where ⇒ is defined as above.

A complete Heyting algebra is a Heyting algebra that is a complete lattice.

In any Heyting algebra, one can define the pseudo-complement ¬x of some element x by setting ¬x=x⇒0, where 0 is the least element of the Heyting algebra.

An element x of a Heyting algebra is called regular if x = ¬¬x.

Properties

Heyting algebras are always distributive. This is sometimes stated as an axiom, but in fact it follows from the existence of relative pseudo-complements. Furthermore, in a complete Heyting algebra, the following infinite distributive law holds:

x∧VY = V{x∧y :  y in Y},

for any element x in H and any subset Y of H.

Not every Heyting algebra satisfies the two De Morgan laws. However, the following statements are equivalent for all Heyting algebras H:

1. H satisfies both De Morgan laws.
2. ¬(x∧y) = ¬x∨¬y, for all x, y in H.
3. ¬x∨¬¬x = 1, for all x in H.
4. ¬¬(x∨y) = ¬¬x∨¬¬y, for all x, y in H.

Boolean algebras are exactly those Heyting algebras in which x = ¬¬x for all x, or, equivalently, in which x ∨ ¬x = 1 for all x. In this case, the element a⇒b is equal to ¬a ∨ b.

In any Heyting algebra, the least and greatest elements 0 and 1 are regular. In addition, the regular elements of any Heyting algebra constitute a Boolean algebra.

Examples

• Every topology provides a complete Heyting algebra in form of its open set lattice. In this case, the element A⇒B is the interior of A^c∪B, where A^c denotes the complement of the open set A. Not all complete Heyting algebras are of this form. These issues are studied in pointless topology, where complete Heyting algebras are also called frames or locales.

• The Lindenbaum algebra of propositional intuitionistic logic is a Heyting algebra. It is defined to be the set of all propositional logic formulae, ordered via logical entailment: for any two formulae F and G we have F≤G iff F|=G. At this stage ≤ is merely a preorder that induces a partial order which is the desired Heyting algebra.