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

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. $a^*=a\to 0$ (equivalence of definitions)
2. $1^*=0$ (if $c=1\to 0$ then $c=c\wedge 1\le 0$ by the definition of $\to$ )
3. $a^*=1$ iff $a=0$ ($1=a\to 0$ implies that $c\wedge a\le 0$ whenever $c\le 1$ In particular $a\le 1$ so $a=a\wedge a\le 0$ or $a=0$ On the other hand, if $a=0$ then $a^*=0^*=0\to 0=1$ )
4. $a\le a^{**}$ and $a^*=a^{***}$ (already true in any pseudocomplemented lattice)
5. $a^*\le a\to b$ (since $a^*\wedge a=0\le b$
6. $(a\to b)\wedge (a\to b^*)=a^*$
   Proof. If $c\wedge a=0$ then $c\wedge a\le b$ so $c\le (a\to b)$ and $c\le (a\to b^*)$ likewise, so $c\le (a\to b)\wedge (a\to b^*)$ This means precisely that $a^*=(a\to b)\wedge (a\to b^*)$
7. $a\to b\le b^*\to a^*$ (since $(a\to b)\wedge b^*\le (a\to b)\wedge (a\to b^*)=a^*)$
8. $a^*\vee b\le a\to b$ (since $b\wedge a\le b$ and $a^* \wedge a=0\le b$

Note that in property 4, $a\le a^{**}$ whereas $a^{**}\le 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 can be shown that if $a^{**}\le 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 $L$ such that $^*$ is a unary operator and $\to$ is a binary operator on $L$ In other words, unlike a morphism between to Heyting lattices, which is nothing more than a lattice homomorphism, a morphism between two Heyting algebras preserves $^*$ and $\to$ Equivalently, a Heyting algebra is a p-algebra with the relative pseudocomplentation opreation $\to$ A lattice homomorphism $f$ preserving $0,1$ and $\to$ is a Heyting algebra homomorphism: since $a^*=a\to 0$ we have $f(a^*)=f(a\to 0)=f(a)\to f(0)=f(a)\to 0=f(a)^*$

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