properties of Heyting algebras
Proposition 1.
Let be a Brouwerian lattice. The following properties hold:
- 1.
- 2.
- 3.
- 4.
Proof.
The first three equations are proved in this entry (http://planetmath.org/BrouwerianLattice). We prove the last equation here. For any , iff iff and iff and iff . Hence the equation holds.∎
Proposition 2.
Conversely, a lattice![]()
with a binary operation
![]()
satisfying the four conditions above is a Brouwerian lattice.
Proof.
Let be a lattice with a binary operation on it satisfying the identities above. We want to show that iff for any . First, suppose . Then . Conversely, suppose . Then by the property 6 in this entry (http://planetmath.org/BrouwerianLattice). As a result, .∎
Corollary 1.
The class of Brouwerian lattices is equational. The class of Heyting algebras![]()
is equational.
Proof.
The first fact is the result of the two propositions above. The second comes from the fact that is not used in the proofs of the propositions.∎
Proposition 3.
Let be a Heyting algebra. Then iff for all .
Proof.
Suppose . Since in any Heyting algebra, we only need to show that . Since is distributive, we have . The last equation comes from the fact that . As a result, . Conversely, suppose . Now, , and therefore .∎
Note, the last inequality in the proof above comes from the inequality , which is a direct consequence of the fact that pseudocomplementation is order-reversing: implies that .
Corollary 2.
A Heyting algebra where psuedocomplentation satisfies the equivalent![]()
conditions above is a Boolean algebra
![]()
. Conversely, a Boolean algebra with is a Heyting algebra.
Proof.
Since and , the pseudocomplementation operation![]()
is the complementation operation. And because any Heyting algebra is distributive, it is Boolean as a result. Conversely, assume is Boolean. Then , so that . On the other hand, if , then .∎
Proposition 4.
A subset of a Heyting algebra is an ultrafilter![]()
iff there is a Heyting algebra homomorphism
with .
Proof.
First, assume is a Heyting algebra homomorphism, and . Clearly, is a filter. Suppose , then . Now, , so . If is not maximal, let be a proper filter containing and , then , so that , and hence , contradicting the fact that is proper. So is maximal.
Conversely, suppose is an ultrafilter of . Define by iff . Let . We first show that is a lattice homomorphism![]()
:
- •
First, iff iff (since is a filter) iff . So respects .
- •
Next, if , then , which means neither nor is in , or that . On the other hand, if , then neither nor is in , since is an ultrafilter. As a result, neither is , which means . So respects .
So is a lattice homomorphism. Next, we show that is a Heyting algebra homomorphism, which means showing that respects : . It suffices to show iff and .
- •
First, if and then and . If , then . Since , , a contradiction

. So .
- •
On the other hand, suppose . So . Now, since , , or . If , then , so there is some with . But this means , or . Since , we would have , a contradiction. Hence .
Therefore is a Heyting algebra homomorphism.∎
In the proof above, we use the fact that, for any ultrafilter in a bounded lattice![]()
, if , then there is such that (for otherwise, the filter generated by and would be proper and properly contains , contradicting the maximality of ). If in addition were distributive, then implies that either or . To see this, suppose . Then there is such that . Similarly, if , there is such that . Let . So , and . Furthermore, . If , so would , a contradiction. Hence .