Heyting algebra

An equivalent definition of Heyting algebras can be given by considering the mappings:

Given a bounded lattice A with largest and smallest elements 1 and 0, and a binary operation →, these together form a Heyting algebra if and only if the following hold:

Of course, if a different set of axioms were chosen for logic, we could modify ours accordingly.

For more on the metaimplication 2 ⇒ 1, see the section "Universal constructions" below.

Heyting algebras are always distributive. Specifically, we always have the identities

By a similar argument, the following infinite distributive law holds in any complete Heyting algebra:

Any complemented element of a Heyting algebra is regular, though the converse is not true in general. In particular, 0 and 1 are always regular.

One of the two De Morgan laws is satisfied in every Heyting algebra, namely

However, the other De Morgan law does not always hold. We have instead a weak de Morgan law:

Heyting algebras satisfying the above properties are related to De Morgan logic in the same way Heyting algebras in general are related to intuitionist logic.

Heyting algebra of propositional formulas in n variables up to intuitionist equivalence