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