A Heyting lattice $L$ is a Brouwerian lattice with a bottom element $0$. Equivalently, $L$ is Heyting iff it is relatively pseudocomplemented and pseudocomplemented iff it is bounded and relatively pseudocomplemented.

Let $a^{*}$ denote the pseudocomplement of $a$ and $a\to b$ the pseudocomplement of $a$ relative to $b$. Then we have the following properties:

1. 1.

   $a^{*}=a\to 0$ (equivalence of definitions)

2. 2.

   $1^{*}=0$ (if $c=1\to 0$, then $c=c\wedge 1\leq 0$ by the definition of $\to$.)

3. 3.

   $a^{*}=1$ iff $a=0$ ($1=a\to 0$ implies that $c\wedge a\leq 0$ whenever $c\leq 1$. In particular $a\leq 1$, so $a=a\wedge a\leq 0$ or $a=0$. On the other hand, if $a=0$, then $a^{*}=0^{*}=0\to 0=1$.)

4. 4.

   $a\leq a^{{**}}$ and $a^{*}=a^{{***}}$ (already true in any pseudocomplemented lattice)

5. 5.

   $a^{*}\leq a\to b$ (since $a^{*}\wedge a=0\leq b$)

6. 6.

   $(a\to b)\wedge(a\to b^{*})=a^{*}$

   Proof.

   If $c\wedge a=0$, then $c\wedge a\leq b$ so $c\leq(a\to b)$, and $c\leq(a\to b^{*})$ likewise, so $c\leq(a\to b)\wedge(a\to b^{*})$. This means precisely that $a^{*}=(a\to b)\wedge(a\to b^{*})$. ∎

7. 7.

   $a\to b\leq b^{*}\to a^{*}$ (since $(a\to b)\wedge b^{*}\leq(a\to b)\wedge(a\to b^{*})=a^{*})$

8. 8.

   $a^{*}\vee b\leq a\to b$ (since $b\wedge a\leq b$ and $a^{*}\wedge a=0\leq b$)

Note that in property 4, $a\leq a^{{**}}$, whereas $a^{{**}}\leq a$ is in general not true, contrasting with the equality $a=a^{{\prime\prime}}$ in a Boolean lattice, where ${}^{{\prime}}$ is the complement operator. It is easy to see that if $a^{{**}}\leq a$ for all $a$ in a Heyting lattice $L$, then $L$ is a Boolean lattice. In this case, the pseudocomplement coincides with the complement of an element $a^{*}=a^{{\prime}}$, and we have the equality in property 7: $a^{*}\vee b=a\to b$, meaning that the concept of relative pseudocomplementation coincides with the material implication in classical propositional logic.

A Heyting algebra is a Heyting lattice $H$ such that $\to$ is a binary operator on $H$. A Heyting algebra homomorphism between two Heyting algebras is a lattice homomorphism that preserves $0,1$, and $\to$. In addition, if $f$ is a Heyting algebra homomorphism, $f$ preserves psudocomplementation: $f(a^{*})=f(a\to 0)=f(a)\to f(0)=f(a)\to 0=f(a)^{*}$.

Remarks.

• In the literature, the assumption that a Heyting algebra contains $0$ is sometimes dropped. Here, we call it a Brouwerian lattice instead.

• Heyting algebras are useful in modeling intuitionistic logic. Every intuitionistic propositional logic can be modelled by a Heyting algebra, and every intuitionistic predicate logic can be modelled by a complete Heyting algebra.